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 --- src/SpecificGen/GF5211_32Reflective/Common.v | 438 +++++++++++++++++++++ src/SpecificGen/GF5211_32Reflective/CommonBinOp.v | 50 +++ src/SpecificGen/GF5211_32Reflective/CommonUnOp.v | 44 +++ .../GF5211_32Reflective/CommonUnOpFEToWire.v | 44 +++ .../GF5211_32Reflective/CommonUnOpFEToZ.v | 44 +++ .../GF5211_32Reflective/CommonUnOpWireToFE.v | 44 +++ src/SpecificGen/GF5211_32Reflective/Reified.v | 13 + src/SpecificGen/GF5211_32Reflective/Reified/Add.v | 12 + .../GF5211_32Reflective/Reified/CarryAdd.v | 17 + .../GF5211_32Reflective/Reified/CarryOpp.v | 17 + .../GF5211_32Reflective/Reified/CarrySub.v | 17 + .../GF5211_32Reflective/Reified/GeModulus.v | 17 + src/SpecificGen/GF5211_32Reflective/Reified/Mul.v | 17 + src/SpecificGen/GF5211_32Reflective/Reified/Opp.v | 12 + src/SpecificGen/GF5211_32Reflective/Reified/Pack.v | 17 + .../GF5211_32Reflective/Reified/PreFreeze.v | 17 + src/SpecificGen/GF5211_32Reflective/Reified/Sub.v | 12 + .../GF5211_32Reflective/Reified/Unpack.v | 17 + 18 files changed, 849 insertions(+) create mode 100644 src/SpecificGen/GF5211_32Reflective/Common.v create mode 100644 src/SpecificGen/GF5211_32Reflective/CommonBinOp.v create mode 100644 src/SpecificGen/GF5211_32Reflective/CommonUnOp.v create mode 100644 src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v create mode 100644 src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v create mode 100644 src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/Add.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/CarryAdd.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/CarryOpp.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/CarrySub.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/GeModulus.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/Mul.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/Opp.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/Pack.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/PreFreeze.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/Sub.v create mode 100644 src/SpecificGen/GF5211_32Reflective/Reified/Unpack.v (limited to 'src/SpecificGen/GF5211_32Reflective') diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v new file mode 100644 index 000000000..a2b9a7c63 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Common.v @@ -0,0 +1,438 @@ +Require Export Coq.ZArith.ZArith. +Require Export Coq.Strings.String. +Require Export Crypto.SpecificGen.GF5211_32. +Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Z.Interpretations. +Require Crypto.Reflection.Z.Interpretations.Relations. +Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Export Crypto.Reflection.Z.Syntax. +Require Import Crypto.Reflection.InterpWfRel. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.MapInterpWf. +Require Import Crypto.Reflection.WfReflective. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Notation Expr := (Expr base_type Word64.interp_base_type op). + +Local Ltac make_type_from uncurried_op := + let T := (type of uncurried_op) in + let T := (eval compute in T) in + let rT := reify_type T in + exact rT. + +Definition ExprBinOpT : type base_type. +Proof. make_type_from (uncurry_binop_fe5211_32 carry_add). Defined. +Definition ExprUnOpT : type base_type. +Proof. make_type_from (uncurry_unop_fe5211_32 carry_opp). Defined. +Definition ExprUnOpFEToZT : type base_type. +Proof. make_type_from (uncurry_unop_fe5211_32 ge_modulus). Defined. +Definition ExprUnOpWireToFET : type base_type. +Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. +Definition ExprUnOpFEToWireT : type base_type. +Proof. make_type_from (uncurry_unop_fe5211_32 pack). Defined. +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. +Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. +Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. +Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. + +Local Ltac bounds_from_list ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}) + | (?x :: ?xs)%list => let bs := bounds_from_list xs in + constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs)) + end. + +Local Ltac make_bounds ls := + compute; + let v := bounds_from_list (List.rev ls) in + let v := (eval compute in v) in + exact v. + +Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. +Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. +Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. +Proof. make_bounds (Tuple.to_list _ bounds). Defined. +Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type. +Proof. make_bounds (Tuple.to_list _ bounds). Defined. +Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type. +Proof. make_bounds (Tuple.to_list _ bounds). Defined. +Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. +Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. + +Definition interp_bexpr : ExprBinOp -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + := fun e => curry_binop_fe5211_32W (Interp (@Word64.interp_op) e). +Definition interp_uexpr : ExprUnOp -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + := fun e => curry_unop_fe5211_32W (Interp (@Word64.interp_op) e). +Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.word64 + := fun e => curry_unop_fe5211_32W (Interp (@Word64.interp_op) e). +Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.wire_digitsW + := fun e => curry_unop_fe5211_32W (Interp (@Word64.interp_op) e). +Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF5211_32BoundedCommon.wire_digitsW -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e). + +Notation binop_correct_and_bounded rop op + := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). +Notation unop_correct_and_bounded rop op + := (iunop_correct_and_bounded (interp_uexpr rop) op) (only parsing). +Notation unop_FEToZ_correct rop op + := (iunop_FEToZ_correct (interp_uexpr_FEToZ rop) op) (only parsing). +Notation unop_FEToWire_correct_and_bounded rop op + := (iunop_FEToWire_correct_and_bounded (interp_uexpr_FEToWire rop) op) (only parsing). +Notation unop_WireToFE_correct_and_bounded rop op + := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). + +Ltac rexpr_cbv := + lazymatch goal with + | [ |- { rexpr | interp_type_gen_rel_pointwise _ (Interp _ (t:=?T) rexpr) (?uncurry ?oper) } ] + => let operf := head oper in + let uncurryf := head uncurry in + try cbv delta [T]; try cbv delta [oper]; + try cbv beta iota delta [uncurryf] + end; + cbv beta iota delta [interp_flat_type Z.interp_base_type interp_base_type zero_]. + +Ltac reify_sig := + rexpr_cbv; eexists; Reify_rhs; reflexivity. + +Local Notation rexpr_sig T uncurried_op := + { rexprZ + | interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op (t:=T) rexprZ) uncurried_op } + (only parsing). + +Notation rexpr_binop_sig op := (rexpr_sig ExprBinOpT (uncurry_binop_fe5211_32 op)) (only parsing). +Notation rexpr_unop_sig op := (rexpr_sig ExprUnOpT (uncurry_unop_fe5211_32 op)) (only parsing). +Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe5211_32 op)) (only parsing). +Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe5211_32 op)) (only parsing). +Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). + +Notation correct_and_bounded_genT ropW'v ropZ_sigv + := (let ropW' := ropW'v in + let ropZ_sig := ropZ_sigv in + let ropW := MapInterp (fun _ x => x) ropW' in + let ropZ := MapInterp Word64.to_Z ropW' in + let ropBounds := MapInterp ZBounds.of_word64 ropW' in + let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in + ropZ = proj1_sig ropZ_sig + /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ) + /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds) + /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW)) + (only parsing). + +Ltac app_tuples x y := + let tx := type of x in + lazymatch (eval hnf in tx) with + | prod _ _ => let xs := app_tuples (snd x) y in + constr:((fst x, xs)) + | _ => constr:((x, y)) + end. + +Local Arguments Tuple.map2 : simpl never. +Local Arguments Tuple.map : simpl never. + +Fixpoint args_to_bounded_helperT {n} + (v : Tuple.tuple' Word64.word64 n) + (bounds : Tuple.tuple' (Z * Z) n) + (pf : List.fold_right + andb true + (Tuple.to_list + _ + (Tuple.map2 + (n:=S n) + (fun bounds v => + let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool) + bounds + (Tuple.map (n:=S n) Word64.word64ToZ v))) = true) + (res : Type) + {struct n} + : Type. +Proof. + refine (match n return (forall (v : Tuple.tuple' _ n) (bounds : Tuple.tuple' _ n), + List.fold_right + _ _ (Tuple.to_list + _ + (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true + -> Type) + with + | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res + | S n' => fun v' bounds' pf0 => let t := _ in + forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res + end v bounds pf). + { clear -pf0. + abstract ( + destruct v', bounds'; simpl @fst; + rewrite Tuple.map_S in pf0; + simpl in pf0; + rewrite Tuple.map2_S in pf0; + simpl @List.fold_right in *; + rewrite Bool.andb_true_iff in pf0; tauto + ). } +Defined. + +Fixpoint args_to_bounded_helper {n} res + {struct n} + : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res. +Proof. + refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with + | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |} + | S n' + => fun v bounds pf f pf' + => @args_to_bounded_helper + n' res (fst v) (fst bounds) _ + (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |})) + end. + { clear -pf pf'. + unfold Tuple.map2, Tuple.map in pf; simpl in *. + abstract ( + destruct bounds; + simpl in *; + rewrite !Bool.andb_true_iff in pf; + destruct_head' and; + Z.ltb_to_lt; auto + ). } + { simpl in *. + clear -pf pf'. + abstract ( + destruct bounds as [? [? ?] ], v; simpl in *; + rewrite Tuple.map_S in pf; simpl in pf; rewrite Tuple.map2_S in pf; + simpl in pf; + rewrite !Bool.andb_true_iff in pf; + destruct_head' and; + Z.ltb_to_lt; auto + ). } +Defined. + +Definition assoc_right'' + := Eval cbv [Tuple.assoc_right' Tuple.rsnoc' fst snd] in @Tuple.assoc_right'. + +Definition args_to_bounded {n} v bounds pf + := Eval cbv [args_to_bounded_helper assoc_right''] in + @args_to_bounded_helper n _ v bounds pf (@assoc_right'' _ _). + +Local Ltac get_len T := + match (eval hnf in T) with + | prod ?A ?B + => let a := get_len A in + let b := get_len B in + (eval compute in (a + b)%nat) + | _ => constr:(1%nat) + end. + +Local Ltac args_to_bounded x H := + let x' := fresh in + set (x' := x); + compute in x; + let len := (let T := type of x in get_len T) in + destruct_head' prod; + let c := constr:(args_to_bounded (n:=pred len) x' _ H) in + let bounds := lazymatch c with args_to_bounded _ ?bounds _ => bounds end in + let c := (eval cbv [all_binders_for ExprUnOpT interp_flat_type args_to_bounded bounds pred fst snd] in c) in + apply c; compute; clear; + try abstract ( + repeat split; + solve [ reflexivity + | refine (fun v => match v with eq_refl => I end) ] + ). + +Definition unop_args_to_bounded (x : fe5211_32W) (H : is_bounded (fe5211_32WToZ x) = true) + : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT). +Proof. args_to_bounded x H. Defined. + +Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true) + : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET). +Proof. args_to_bounded x H. Defined. +Definition binop_args_to_bounded (x : fe5211_32W * fe5211_32W) + (H : is_bounded (fe5211_32WToZ (fst x)) = true) + (H' : is_bounded (fe5211_32WToZ (snd x)) = true) + : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT). +Proof. + let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in + exact v. +Defined. + +Ltac assoc_right_tuple x so_far := + let t := type of x in + lazymatch (eval hnf in t) with + | prod _ _ => let so_far := assoc_right_tuple (snd x) so_far in + assoc_right_tuple (fst x) so_far + | _ => lazymatch so_far with + | @None => x + | _ => constr:((x, so_far)) + end + end. + +Local Ltac make_bounds_prop bounds orig_bounds := + let bounds' := fresh "bounds'" in + let bounds_bad := fresh "bounds_bad" in + rename bounds into bounds_bad; + let boundsv := assoc_right_tuple bounds_bad (@None) in + pose boundsv as bounds; + pose orig_bounds as bounds'; + repeat (refine (match fst bounds' with + | Some bounds' => let (l, u) := fst bounds in + let (l', u') := bounds' in + ((l' <=? l) && (u <=? u'))%Z%bool + | None => false + end && _)%bool; + destruct bounds' as [_ bounds'], bounds as [_ bounds]); + try exact (match bounds' with + | Some bounds' => let (l, u) := bounds in + let (l', u') := bounds' in + ((l' <=? l) && (u <=? u'))%Z%bool + | None => false + end). + +Definition unop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpT)) : bool. +Proof. make_bounds_prop bounds ExprUnOp_bounds. Defined. +Definition binop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprBinOpT)) : bool. +Proof. make_bounds_prop bounds ExprUnOp_bounds. Defined. +Definition unopFEToWire_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpFEToWireT)) : bool. +Proof. make_bounds_prop bounds ExprUnOpWireToFE_bounds. Defined. +Definition unopWireToFE_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpWireToFET)) : bool. +Proof. make_bounds_prop bounds ExprUnOp_bounds. Defined. +(* TODO FIXME(jgross?, andreser?): Is every function returning a single Z a boolean function? *) +Definition unopFEToZ_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpFEToZT)) : bool. +Proof. + refine (let (l, u) := bounds in ((0 <=? l) && (u <=? 1))%Z%bool). +Defined. + +(* FIXME TODO(jgross): This is a horrible tactic. We should unify the + various kinds of correct and boundedness, and abstract in Gallina + rather than Ltac *) + +Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := + let Heq := fresh "Heq" in + let Hbounds0 := fresh "Hbounds0" in + let Hbounds1 := fresh "Hbounds1" in + let Hbounds2 := fresh "Hbounds2" in + pose proof (proj2_sig ropZ_sig) as Heq; + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE + curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW + curry_binop_fe5211_32 curry_unop_fe5211_32 curry_unop_wire_digits + uncurry_binop_fe5211_32W uncurry_unop_fe5211_32W uncurry_unop_wire_digitsW + uncurry_binop_fe5211_32 uncurry_unop_fe5211_32 uncurry_unop_wire_digits + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET + interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; + cbv zeta in *; + simpl @fe5211_32WToZ; simpl @wire_digitsWToZ; + rewrite <- Heq; clear Heq; + destruct Hbounds as [Heq Hbounds]; + change interp_op with (@Z.interp_op) in *; + change interp_base_type with (@Z.interp_base_type) in *; + rewrite <- Heq; clear Heq; + destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ]; + pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left; + pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right; + specialize_by repeat first [ progress intros + | reflexivity + | assumption + | progress destruct_head' base_type + | progress destruct_head' BoundedWord64.BoundedWord + | progress destruct_head' and + | progress repeat apply conj ]; + specialize (Hbounds_left args H0); + specialize (Hbounds_right args H0); + cbv beta in *; + lazymatch type of Hbounds_right with + | match ?e with _ => _ end + => lazymatch type of H1 with + | match ?e' with _ => _ end + => change e' with e in H1; destruct e eqn:?; [ | exfalso; assumption ] + end + end; + repeat match goal with x := _ |- _ => subst x end; + cbv [id + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded + Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right; + match goal with + | [ |- fe5211_32WToZ ?x = _ /\ _ ] + => destruct x; destruct_head_hnf' prod + | [ |- wire_digitsWToZ ?x = _ /\ _ ] + => destruct x; destruct_head_hnf' prod + | [ |- _ = _ ] + => exact Hbounds_left + end; + change word64ToZ with Word64.word64ToZ in *; + (split; [ exact Hbounds_left | ]); + cbv [interp_flat_type] in *; + cbv [fst snd + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds] in H1; + destruct_head' ZBounds.bounds; + unfold_is_bounded_in H1; + simpl @fe5211_32WToZ; simpl @wire_digitsWToZ; + unfold_is_bounded; + destruct_head' and; + Z.ltb_to_lt; + change Word64.word64ToZ with word64ToZ in *; + repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity. + + +Ltac rexpr_correct := + let ropW' := fresh in + let ropZ_sig := fresh in + intros ropW' ropZ_sig; + let wf_ropW := fresh "wf_ropW" in + assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); + cbv zeta; repeat apply conj; + [ vm_compute; reflexivity + | apply @InterpRelWf; + [ | apply @RelWfMapInterp, wf_ropW ].. ]; + auto with interp_related. + +Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing). + +Notation compute_bounds opW bounds + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds) + (only parsing). + + +Module Export PrettyPrinting. + (* We add [enlargen] to force [bounds_on] to be in [Type] in 8.4 and + 8.5/8.6. Because [Set] is special and things break if + [bounds_on] ends up in [Set] for reasons jgross hasn't bothered + to debug. *) + Inductive bounds_on := overflow | in_range (lower upper : Z) | enlargen (_ : Set). + + Inductive result := yes | no | borked. + + Definition ZBounds_to_bounds_on + := fun t : base_type + => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with + | TZ => fun x => match x with + | Some {| ZBounds.lower := l ; ZBounds.upper := u |} + => in_range l u + | None + => overflow + end + end. + + Fixpoint does_it_overflow {t} : interp_flat_type (fun t => match t with TZ => bounds_on end) t -> result + := match t return interp_flat_type (fun t => match t with TZ => bounds_on end) t -> result with + | Tbase TZ => fun v => match v with + | overflow => yes + | in_range _ _ => no + | enlargen _ => borked + end + | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with + | no, no => no + | yes, no | no, yes | yes, yes => yes + | borked, _ | _, borked => borked + end + end. + + (** This gives a slightly easier to read version of the bounds *) + Notation compute_bounds_for_display opW bounds + := (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) (only parsing). + Notation sanity_compute opW bounds + := (does_it_overflow (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds))) (only parsing). + Notation sanity_check opW bounds + := (eq_refl (sanity_compute opW bounds) <: no = no) (only parsing). +End PrettyPrinting. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v new file mode 100644 index 000000000..a6a6e0f28 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v @@ -0,0 +1,50 @@ +Require Export Crypto.SpecificGen.GF5211_32Reflective.Common. +Require Import Crypto.SpecificGen.GF5211_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 ExprBinOp_correct_and_bounded + ropW op (ropZ_sig : rexpr_binop_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall xy + (xy := (eta_fe5211_32W (fst xy), eta_fe5211_32W (snd xy))) + (Hxy : is_bounded (fe5211_32WToZ (fst xy)) = true + /\ is_bounded (fe5211_32WToZ (snd xy)) = true), + let Hx := let (Hx, Hy) := Hxy in Hx in + let Hy := let (Hx, Hy) := Hxy in Hy in + let args := binop_args_to_bounded xy Hx Hy 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 xy + (xy := (eta_fe5211_32W (fst xy), eta_fe5211_32W (snd xy))) + (Hxy : is_bounded (fe5211_32WToZ (fst xy)) = true + /\ is_bounded (fe5211_32WToZ (snd xy)) = true), + let Hx := let (Hx, Hy) := Hxy in Hx in + let Hy := let (Hx, Hy) := Hxy in Hy in + let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy 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 => binop_bounds_good bounds = true + | None => False + end) + : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x y Hx Hy. + pose x as x'; pose y as y'. + hnf in x, y; destruct_head' prod. + specialize (H0 (x', y') (conj Hx Hy)). + specialize (H1 (x', y') (conj Hx Hy)). + let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v new file mode 100644 index 000000000..9a1d5bdef --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v @@ -0,0 +1,44 @@ +Require Export Crypto.SpecificGen.GF5211_32Reflective.Common. +Require Import Crypto.SpecificGen.GF5211_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 ExprUnOp_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe5211_32W x) + (Hx : is_bounded (fe5211_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_fe5211_32W x) + (Hx : is_bounded (fe5211_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 => unop_bounds_good bounds = true + | None => False + end) + : unop_correct_and_bounded (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. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v new file mode 100644 index 000000000..14f3d3dd7 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v @@ -0,0 +1,44 @@ +Require Export Crypto.SpecificGen.GF5211_32Reflective.Common. +Require Import Crypto.SpecificGen.GF5211_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 ExprUnOpFEToWire_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe5211_32W x) + (Hx : is_bounded (fe5211_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_fe5211_32W x) + (Hx : is_bounded (fe5211_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 => unopFEToWire_bounds_good bounds = true + | None => False + end) + : unop_FEToWire_correct_and_bounded (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. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v new file mode 100644 index 000000000..ab44167a6 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v @@ -0,0 +1,44 @@ +Require Export Crypto.SpecificGen.GF5211_32Reflective.Common. +Require Import Crypto.SpecificGen.GF5211_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_fe5211_32W x) + (Hx : is_bounded (fe5211_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_fe5211_32W x) + (Hx : is_bounded (fe5211_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. diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v new file mode 100644 index 000000000..9948ea3a0 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v @@ -0,0 +1,44 @@ +Require Export Crypto.SpecificGen.GF5211_32Reflective.Common. +Require Import Crypto.SpecificGen.GF5211_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 ExprUnOpWireToFE_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_wire_digitsW x) + (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), + let args := unopWireToFE_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_wire_digitsW x) + (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), + let args := unopWireToFE_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 => unopWireToFE_bounds_good bounds = true + | None => False + end) + : unop_WireToFE_correct_and_bounded (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:(unopWireToFE_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/SpecificGen/GF5211_32Reflective/Reified.v b/src/SpecificGen/GF5211_32Reflective/Reified.v new file mode 100644 index 000000000..a783188c9 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified.v @@ -0,0 +1,13 @@ +(** We split the reification up into separate files, one operation per + file, so that it can run in parallel. *) +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.Add. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.CarryAdd. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.Sub. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.CarrySub. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.Mul. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.Opp. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.CarryOpp. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.PreFreeze. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.GeModulus. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.Pack. +Require Export Crypto.SpecificGen.GF5211_32Reflective.Reified.Unpack. diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/Add.v b/src/SpecificGen/GF5211_32Reflective/Reified/Add.v new file mode 100644 index 000000000..5ddd88689 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/Add.v @@ -0,0 +1,12 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonBinOp. + +Definition raddZ_sig : rexpr_binop_sig add. Proof. reify_sig. Defined. +Definition raddW := Eval vm_compute in rword_of_Z raddZ_sig. +Lemma raddW_correct_and_bounded_gen : correct_and_bounded_genT raddW raddZ_sig. +Proof. rexpr_correct. Qed. +Definition radd_output_bounds := Eval vm_compute in compute_bounds raddW ExprBinOp_bounds. + +Local Open Scope string_scope. +Compute ("Add", compute_bounds_for_display raddW ExprBinOp_bounds). +Compute ("Add overflows? ", sanity_compute raddW ExprBinOp_bounds). +Compute ("Add overflows (error if it does)? ", sanity_check raddW ExprBinOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/CarryAdd.v b/src/SpecificGen/GF5211_32Reflective/Reified/CarryAdd.v new file mode 100644 index 000000000..3b17ad60c --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/CarryAdd.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonBinOp. + +Definition rcarry_addZ_sig : rexpr_binop_sig carry_add. Proof. reify_sig. Defined. +Definition rcarry_addW := Eval vm_compute in rword_of_Z rcarry_addZ_sig. +Lemma rcarry_addW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_addW rcarry_addZ_sig. +Proof. rexpr_correct. Qed. +Definition rcarry_add_output_bounds := Eval vm_compute in compute_bounds rcarry_addW ExprBinOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rcarry_addW_correct_and_bounded + := ExprBinOp_correct_and_bounded + rcarry_addW carry_add rcarry_addZ_sig rcarry_addW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Carry_Add", compute_bounds_for_display rcarry_addW ExprBinOp_bounds). +Compute ("Carry_Add overflows? ", sanity_compute rcarry_addW ExprBinOp_bounds). +Compute ("Carry_Add overflows (error if it does)? ", sanity_check rcarry_addW ExprBinOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/CarryOpp.v b/src/SpecificGen/GF5211_32Reflective/Reified/CarryOpp.v new file mode 100644 index 000000000..faf4f7533 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/CarryOpp.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonUnOp. + +Definition rcarry_oppZ_sig : rexpr_unop_sig carry_opp. Proof. reify_sig. Defined. +Definition rcarry_oppW := Eval vm_compute in rword_of_Z rcarry_oppZ_sig. +Lemma rcarry_oppW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_oppW rcarry_oppZ_sig. +Proof. rexpr_correct. Qed. +Definition rcarry_opp_output_bounds := Eval vm_compute in compute_bounds rcarry_oppW ExprUnOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rcarry_oppW_correct_and_bounded + := ExprUnOp_correct_and_bounded + rcarry_oppW carry_opp rcarry_oppZ_sig rcarry_oppW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Carry_Opp", compute_bounds_for_display rcarry_oppW ExprUnOp_bounds). +Compute ("Carry_Opp overflows? ", sanity_compute rcarry_oppW ExprUnOp_bounds). +Compute ("Carry_Opp overflows (error if it does)? ", sanity_check rcarry_oppW ExprUnOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/CarrySub.v b/src/SpecificGen/GF5211_32Reflective/Reified/CarrySub.v new file mode 100644 index 000000000..ad75f4530 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/CarrySub.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonBinOp. + +Definition rcarry_subZ_sig : rexpr_binop_sig carry_sub. Proof. reify_sig. Defined. +Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig. +Lemma rcarry_subW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_subW rcarry_subZ_sig. +Proof. rexpr_correct. Qed. +Definition rcarry_sub_output_bounds := Eval vm_compute in compute_bounds rcarry_subW ExprBinOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rcarry_subW_correct_and_bounded + := ExprBinOp_correct_and_bounded + rcarry_subW carry_sub rcarry_subZ_sig rcarry_subW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Carry_Sub", compute_bounds_for_display rcarry_subW ExprBinOp_bounds). +Compute ("Carry_Sub overflows? ", sanity_compute rcarry_subW ExprBinOp_bounds). +Compute ("Carry_Sub overflows (error if it does)? ", sanity_check rcarry_subW ExprBinOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/GeModulus.v b/src/SpecificGen/GF5211_32Reflective/Reified/GeModulus.v new file mode 100644 index 000000000..68b630622 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/GeModulus.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonUnOpFEToZ. + +Definition rge_modulusZ_sig : rexpr_unop_FEToZ_sig ge_modulus. Proof. reify_sig. Defined. +Definition rge_modulusW := Eval vm_compute in rword_of_Z rge_modulusZ_sig. +Lemma rge_modulusW_correct_and_bounded_gen : correct_and_bounded_genT rge_modulusW rge_modulusZ_sig. +Proof. rexpr_correct. Qed. +Definition rge_modulus_output_bounds := Eval vm_compute in compute_bounds rge_modulusW ExprUnOpFEToZ_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rge_modulusW_correct_and_bounded + := ExprUnOpFEToZ_correct_and_bounded + rge_modulusW ge_modulus rge_modulusZ_sig rge_modulusW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Ge_Modulus", compute_bounds_for_display rge_modulusW ExprUnOpFEToZ_bounds). +Compute ("Ge_Modulus overflows? ", sanity_compute rge_modulusW ExprUnOpFEToZ_bounds). +Compute ("Ge_Modulus overflows (error if it does)? ", sanity_check rge_modulusW ExprUnOpFEToZ_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/Mul.v b/src/SpecificGen/GF5211_32Reflective/Reified/Mul.v new file mode 100644 index 000000000..b6d2170de --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/Mul.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonBinOp. + +Definition rmulZ_sig : rexpr_binop_sig mul. Proof. reify_sig. Defined. +Definition rmulW := Eval vm_compute in rword_of_Z rmulZ_sig. +Lemma rmulW_correct_and_bounded_gen : correct_and_bounded_genT rmulW rmulZ_sig. +Proof. rexpr_correct. Qed. +Definition rmul_output_bounds := Eval vm_compute in compute_bounds rmulW ExprBinOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rmulW_correct_and_bounded + := ExprBinOp_correct_and_bounded + rmulW mul rmulZ_sig rmulW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds). +Compute ("Mul overflows? ", sanity_compute rmulW ExprBinOp_bounds). +Compute ("Mul overflows (error if it does)? ", sanity_check rmulW ExprBinOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/Opp.v b/src/SpecificGen/GF5211_32Reflective/Reified/Opp.v new file mode 100644 index 000000000..ae3389010 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/Opp.v @@ -0,0 +1,12 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonUnOp. + +Definition roppZ_sig : rexpr_unop_sig opp. Proof. reify_sig. Defined. +Definition roppW := Eval vm_compute in rword_of_Z roppZ_sig. +Lemma roppW_correct_and_bounded_gen : correct_and_bounded_genT roppW roppZ_sig. +Proof. rexpr_correct. Qed. +Definition ropp_output_bounds := Eval vm_compute in compute_bounds roppW ExprUnOp_bounds. + +Local Open Scope string_scope. +Compute ("Opp", compute_bounds_for_display roppW ExprUnOp_bounds). +Compute ("Opp overflows? ", sanity_compute roppW ExprUnOp_bounds). +Compute ("Opp overflows (error if it does)? ", sanity_check roppW ExprUnOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/Pack.v b/src/SpecificGen/GF5211_32Reflective/Reified/Pack.v new file mode 100644 index 000000000..108ce3578 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/Pack.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonUnOpFEToWire. + +Definition rpackZ_sig : rexpr_unop_FEToWire_sig pack. Proof. reify_sig. Defined. +Definition rpackW := Eval vm_compute in rword_of_Z rpackZ_sig. +Lemma rpackW_correct_and_bounded_gen : correct_and_bounded_genT rpackW rpackZ_sig. +Proof. rexpr_correct. Qed. +Definition rpack_output_bounds := Eval vm_compute in compute_bounds rpackW ExprUnOpFEToWire_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rpackW_correct_and_bounded + := ExprUnOpFEToWire_correct_and_bounded + rpackW pack rpackZ_sig rpackW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds). +Compute ("Pack overflows? ", sanity_compute rpackW ExprUnOpFEToWire_bounds). +Compute ("Pack overflows (error if it does)? ", sanity_check rpackW ExprUnOpFEToWire_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/PreFreeze.v b/src/SpecificGen/GF5211_32Reflective/Reified/PreFreeze.v new file mode 100644 index 000000000..4788f9f1a --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/PreFreeze.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonUnOp. + +Definition rprefreezeZ_sig : rexpr_unop_sig prefreeze. Proof. cbv [prefreeze GF5211_32.prefreeze]. reify_sig. Defined. +Definition rprefreezeW := Eval vm_compute in rword_of_Z rprefreezeZ_sig. +Lemma rprefreezeW_correct_and_bounded_gen : correct_and_bounded_genT rprefreezeW rprefreezeZ_sig. +Proof. rexpr_correct. Qed. +Definition rprefreeze_output_bounds := Eval vm_compute in compute_bounds rprefreezeW ExprUnOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rprefreezeW_correct_and_bounded + := ExprUnOp_correct_and_bounded + rprefreezeW prefreeze rprefreezeZ_sig rprefreezeW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("PreFreeze", compute_bounds_for_display rprefreezeW ExprUnOp_bounds). +Compute ("PreFreeze overflows? ", sanity_compute rprefreezeW ExprUnOp_bounds). +Compute ("PreFreeze overflows (error if it does)? ", sanity_check rprefreezeW ExprUnOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/Sub.v b/src/SpecificGen/GF5211_32Reflective/Reified/Sub.v new file mode 100644 index 000000000..f0c1f5d27 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/Sub.v @@ -0,0 +1,12 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonBinOp. + +Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined. +Definition rsubW := Eval vm_compute in rword_of_Z rsubZ_sig. +Lemma rsubW_correct_and_bounded_gen : correct_and_bounded_genT rsubW rsubZ_sig. +Proof. rexpr_correct. Qed. +Definition rsub_output_bounds := Eval vm_compute in compute_bounds rsubW ExprBinOp_bounds. + +Local Open Scope string_scope. +Compute ("Sub", compute_bounds_for_display rsubW ExprBinOp_bounds). +Compute ("Sub overflows? ", sanity_compute rsubW ExprBinOp_bounds). +Compute ("Sub overflows (error if it does)? ", sanity_check rsubW ExprBinOp_bounds). diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/Unpack.v b/src/SpecificGen/GF5211_32Reflective/Reified/Unpack.v new file mode 100644 index 000000000..1040ec6d2 --- /dev/null +++ b/src/SpecificGen/GF5211_32Reflective/Reified/Unpack.v @@ -0,0 +1,17 @@ +Require Import Crypto.SpecificGen.GF5211_32Reflective.CommonUnOpWireToFE. + +Definition runpackZ_sig : rexpr_unop_WireToFE_sig unpack. Proof. reify_sig. Defined. +Definition runpackW := Eval vm_compute in rword_of_Z runpackZ_sig. +Lemma runpackW_correct_and_bounded_gen : correct_and_bounded_genT runpackW runpackZ_sig. +Proof. rexpr_correct. Qed. +Definition runpack_output_bounds := Eval vm_compute in compute_bounds runpackW ExprUnOpWireToFE_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition runpackW_correct_and_bounded + := ExprUnOpWireToFE_correct_and_bounded + runpackW unpack runpackZ_sig runpackW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds). +Compute ("Unpack overflows? ", sanity_compute runpackW ExprUnOpWireToFE_bounds). +Compute ("Unpack overflows (error if it does)? ", sanity_check runpackW ExprUnOpWireToFE_bounds). -- cgit v1.2.3