diff options
Diffstat (limited to 'src/SpecificGen/GF5211_32BoundedCommon.v')
| -rw-r--r-- | src/SpecificGen/GF5211_32BoundedCommon.v | 819 |
1 files changed, 0 insertions, 819 deletions
diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v deleted file mode 100644 index 2ecc4ed1c..000000000 --- a/src/SpecificGen/GF5211_32BoundedCommon.v +++ /dev/null @@ -1,819 +0,0 @@ -Require Import Coq.Classes.Morphisms. -Require Import Crypto.BaseSystem. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. -Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. -Require Import Crypto.SpecificGen.GF5211_32. -Require Import Bedrock.Word Crypto.Util.WordUtil. -Require Import Coq.Lists.List Crypto.Util.ListUtil. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.HList. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Algebra. -Import ListNotations. -Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Local Open Scope Z. - -(* BEGIN common curve-specific definitions *) -Definition bit_width : nat := Eval compute in Z.to_nat (GF5211_32.int_width). -Local Notation b_of exp := (0, 2^exp + 2^(exp-3))%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) -Definition bounds_exp : tuple Z length_fe5211_32 - := Eval compute in - Tuple.from_list length_fe5211_32 limb_widths eq_refl. -Definition bounds : tuple (Z * Z) length_fe5211_32 - := Eval compute in - Tuple.map (fun e => b_of e) bounds_exp. -Definition wire_digit_bounds_exp : tuple Z (length wire_widths) - := Eval compute in Tuple.from_list _ wire_widths eq_refl. -Definition wire_digit_bounds : tuple (Z * Z) (length wire_widths) - := Eval compute in Tuple.map (fun e => (0,2^e-1)%Z) wire_digit_bounds_exp. -(* END common curve-specific definitions *) - -(* BEGIN aliases for word extraction *) -Definition word64 := Word.word bit_width. -Coercion word64ToZ (x : word64) : Z := Z.of_N (wordToN x). -Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x). -Definition NToWord64 : N -> word64 := NToWord _. -Definition word64ize (x : word64) : word64 - := Eval cbv [wordToN N.succ_double N.double] in NToWord64 (wordToN x). -Definition w64eqb (x y : word64) := weqb x y. - -Global Arguments NToWord64 : simpl never. -Arguments word64 : simpl never. -Arguments bit_width : simpl never. -Global Opaque word64. -Global Opaque bit_width. - -(* END aliases for word extraction *) - -(* BEGIN basic types *) -Module Type WordIsBounded. - Parameter is_boundedT : forall (lower upper : Z), word64 -> bool. - Parameter Build_is_boundedT : forall {lower upper} {proj_word : word64}, - andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true -> is_boundedT lower upper proj_word = true. - Parameter project_is_boundedT : forall {lower upper} {proj_word : word64}, - is_boundedT lower upper proj_word = true -> andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true. -End WordIsBounded. - -Module Import WordIsBoundedDefault : WordIsBounded. - Definition is_boundedT : forall (lower upper : Z), word64 -> bool - := fun lower upper proj_word => andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z. - Definition Build_is_boundedT {lower upper} {proj_word : word64} - : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true -> is_boundedT lower upper proj_word = true - := fun x => x. - Definition project_is_boundedT {lower upper} {proj_word : word64} - : is_boundedT lower upper proj_word = true -> andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true - := fun x => x. -End WordIsBoundedDefault. - -Definition bounded_word (lower upper : Z) - := { proj_word : word64 | is_boundedT lower upper proj_word = true }. -Local Notation word_of exp := (bounded_word (fst (b_of exp)) (snd (b_of exp))). -Local Notation unbounded_word sz := (bounded_word 0 (2^sz-1)%Z). - -Local Opaque word64. -Definition fe5211_32W := Eval cbv (*-[word64]*) in (tuple word64 length_fe5211_32). -Definition wire_digitsW := Eval cbv (*-[word64]*) in (tuple word64 (length wire_widths)). -Definition fe5211_32 := - Eval cbv -[bounded_word Z.pow Z.sub Z.add] in - hlist (fun e => word_of e) bounds_exp. -Definition wire_digits := - Eval cbv -[bounded_word Z.pow Z.sub Z.add] in - hlist (fun e => unbounded_word e) wire_digit_bounds_exp. - -Definition is_bounded_gen {n} (x : tuple Z n) (bounds : tuple (Z * Z) n) : bool - := let res := Tuple.map2 - (fun bounds v => - let '(lower, upper) := bounds in - (lower <=? v) && (v <=? upper))%bool%Z - bounds x in - List.fold_right andb true (Tuple.to_list _ res). - -Definition is_bounded (x : SpecificGen.GF5211_32.fe5211_32) : bool - := is_bounded_gen (n:=length_fe5211_32) x bounds. - -Definition wire_digits_is_bounded (x : SpecificGen.GF5211_32.wire_digits) : bool - := is_bounded_gen (n:=length wire_widths) x wire_digit_bounds. - -(* END basic types *) - -Section generic_destructuring. - Fixpoint app_on' A n : forall T (f : tuple' A n) (P : forall x : tuple' A n, T x), T f - := match n return forall T (f : tuple' A n) (P : forall x : tuple' A n, T x), T f with - | O => fun T v P => P v - | S n' => fun T v P => let '(v, x) := v in app_on' A n' _ v (fun v => P (v, x)) - end. - Definition app_on {A n} : forall {T} (f : tuple A n) (P : forall x : tuple A n, T x), T f - := match n return forall T (f : tuple A n) (P : forall x : tuple A n, T x), T f with - | O => fun T v P => P v - | S n' => @app_on' A n' - end. - Lemma app_on'_correct {A n T} f (P : forall x : tuple' A n, T x) : app_on' A n T f P = P f. - Proof. - induction n; simpl in *; destruct_head' prod; [ reflexivity | exact (IHn _ _ (fun t => P (t, _))) ]. - Qed. - Lemma app_on_correct {A n T} f (P : forall x : tuple A n, T x) : app_on f P = P f. - Proof. destruct n; [ reflexivity | apply app_on'_correct ]. Qed. - - Fixpoint app_on_h' A F n : forall ts T (f : @hlist' A n F ts) (P : forall x : @hlist' A n F ts, T x), T f - := match n return forall ts T (f : @hlist' A n F ts) (P : forall x : @hlist' A n F ts, T x), T f with - | O => fun ts T v P => P v - | S n' => fun ts T v P => let '(v, x) := v in app_on_h' A F n' _ _ v (fun v => P (v, x)) - end. - Definition app_on_h {A F n} : forall ts T (f : @hlist A n F ts) (P : forall x : @hlist A n F ts, T x), T f - := match n return forall ts T (f : @hlist A n F ts) (P : forall x : @hlist A n F ts, T x), T f with - | O => fun ts T v P => P v - | S n' => @app_on_h' A F n' - end. - Lemma app_on_h'_correct {A F n ts T} f P : @app_on_h' A F n ts T f P = P f. - Proof. - induction n; simpl in *; destruct_head' prod; [ reflexivity | exact (IHn _ _ _ (fun h => P (h, f))) ]. - Qed. - Lemma app_on_h_correct {A} F {n} ts {T} f P : @app_on_h A F n ts T f P = P f. - Proof. destruct n; [ reflexivity | apply app_on_h'_correct ]. Qed. - - Definition app_wire_digitsW_dep {A T} (P : forall x : tuple A (length wire_widths), T x) - : forall (f : tuple A (length wire_widths)), T f - := Eval compute in fun f => @app_on A (length wire_widths) T f P. - Definition app_wire_digitsW {A T} (f : tuple A (length wire_widths)) (P : tuple A (length wire_widths) -> T) - := Eval compute in @app_wire_digitsW_dep A (fun _ => T) P f. - Definition app_fe5211_32W_dep {A T} (P : forall x : tuple A length_fe5211_32, T x) - : forall (f : tuple A length_fe5211_32), T f - := Eval compute in fun f => @app_on A length_fe5211_32 T f P. - Definition app_fe5211_32W {A T} (f : tuple A length_fe5211_32) (P : tuple A length_fe5211_32 -> T) - := Eval compute in @app_fe5211_32W_dep A (fun _ => T) P f. - Definition app_fe5211_32_dep {T} (P : forall x : fe5211_32, T x) - : forall f : fe5211_32, T f - := Eval compute in fun f => @app_on_h _ (fun e => word_of e) length_fe5211_32 bounds_exp T f P. - Definition app_fe5211_32 {T} (f : fe5211_32) (P : hlist (fun e => word_of e) bounds_exp -> T) - := Eval compute in @app_fe5211_32_dep (fun _ => T) P f. - Definition app_wire_digits_dep {T} (P : forall x : wire_digits, T x) - : forall f : wire_digits, T f - := Eval compute in fun f => @app_on_h _ (fun e => unbounded_word e) (length wire_widths) wire_digit_bounds_exp T f P. - Definition app_wire_digits {T} (f : wire_digits) (P : hlist (fun e => unbounded_word e) wire_digit_bounds_exp -> T) - := Eval compute in @app_wire_digits_dep (fun _ => T) P f. - - Definition app_wire_digitsW_dep_correct {A T} f P : @app_wire_digitsW_dep A T P f = P f - := app_on_correct f P. - Definition app_wire_digitsW_correct {A T} f P : @app_wire_digitsW A T f P = P f - := @app_wire_digitsW_dep_correct A (fun _ => T) f P. - Definition app_fe5211_32W_dep_correct {A T} f P : @app_fe5211_32W_dep A T P f = P f - := app_on_correct f P. - Definition app_fe5211_32W_correct {A T} f P : @app_fe5211_32W A T f P = P f - := @app_fe5211_32W_dep_correct A (fun _ => T) f P. - Definition app_fe5211_32_dep_correct {T} f P : @app_fe5211_32_dep T P f = P f - := app_on_h_correct (fun e => word_of e) bounds_exp f P. - Definition app_fe5211_32_correct {T} f P : @app_fe5211_32 T f P = P f - := @app_fe5211_32_dep_correct (fun _ => T) f P. - Definition app_wire_digits_dep_correct {T} f P : @app_wire_digits_dep T P f = P f - := app_on_h_correct (fun e => unbounded_word e) wire_digit_bounds_exp f P. - Definition app_wire_digits_correct {T} f P : @app_wire_digits T f P = P f - := @app_wire_digits_dep_correct (fun _ => T) f P. - - Definition appify2 {T} (op : fe5211_32W -> fe5211_32W -> T) (f g : fe5211_32W) := - app_fe5211_32W f (fun f0 => (app_fe5211_32W g (fun g0 => op f0 g0))). - - Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. - Proof. - intros. cbv [appify2]. - etransitivity; apply app_fe5211_32W_correct. - Qed. - - Definition appify9 {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32W) := - app_fe5211_32W x0 (fun x0' => - app_fe5211_32W x1 (fun x1' => - app_fe5211_32W x2 (fun x2' => - app_fe5211_32W x3 (fun x3' => - app_fe5211_32W x4 (fun x4' => - app_fe5211_32W x5 (fun x5' => - app_fe5211_32W x6 (fun x6' => - app_fe5211_32W x7 (fun x7' => - app_fe5211_32W x8 (fun x8' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))). - - Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8, - @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8. - Proof. - intros. cbv [appify9]. - repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity. - Qed. -End generic_destructuring. - -Definition eta_fe5211_32W_sig (x : fe5211_32W) : { v : fe5211_32W | v = x }. -Proof. - eexists; symmetry. - repeat (etransitivity; [ apply surjective_pairing | apply f_equal2 ]); reflexivity. -Defined. -Definition eta_fe5211_32W (x : fe5211_32W) : fe5211_32W - := Eval cbv [proj1_sig eta_fe5211_32W_sig] in proj1_sig (eta_fe5211_32W_sig x). -Definition eta_wire_digitsW_sig (x : wire_digitsW) : { v : wire_digitsW | v = x }. -Proof. - eexists; symmetry. - repeat (etransitivity; [ apply surjective_pairing | apply f_equal2 ]); reflexivity. -Defined. -Definition eta_wire_digitsW (x : wire_digitsW) : wire_digitsW - := Eval cbv [proj1_sig eta_wire_digitsW_sig] in proj1_sig (eta_wire_digitsW_sig x). - -Local Transparent word64. -Lemma word64ize_id x : word64ize x = x. -Proof. apply NToWord_wordToN. Qed. -Local Opaque word64. - -Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y. -Proof. apply wordeqb_Zeqb. Qed. - -Local Arguments Z.pow_pos !_ !_ / . -Lemma word64ToZ_ZToWord64 x : 0 <= x < 2^Z.of_nat bit_width -> word64ToZ (ZToWord64 x) = x. -Proof. - intros; unfold word64ToZ, ZToWord64. - rewrite wordToN_NToWord_idempotent, Z2N.id - by (omega || apply N2Z.inj_lt; rewrite <- ?(N_nat_Z (Npow2 _)), ?Npow2_nat, ?Zpow_pow2, ?N2Z.id, ?Z2N.id, ?Z2Nat.id by omega; omega). - reflexivity. -Qed. -Lemma ZToWord64_word64ToZ x : ZToWord64 (word64ToZ x) = x. -Proof. - intros; unfold word64ToZ, ZToWord64. - rewrite N2Z.id, NToWord_wordToN; reflexivity. -Qed. - -(* BEGIN precomputation. *) - -Definition proj_word {lower upper} (v : bounded_word lower upper) := Eval cbv [proj1_sig] in proj1_sig v. -Definition word_bounded {lower upper} (v : bounded_word lower upper) - : andb (lower <=? proj_word v)%Z (proj_word v <=? upper)%Z = true - := project_is_boundedT (proj2_sig v). -Definition Build_bounded_word' {lower upper} proj_word word_bounded : bounded_word lower upper - := exist _ proj_word (Build_is_boundedT word_bounded). -Arguments proj_word {_ _} _. -Arguments word_bounded {_ _} _. -Arguments Build_bounded_word' {_ _} _ _. -Definition Build_bounded_word {lower upper} (proj_word : word64) (word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true) - : bounded_word lower upper - := Build_bounded_word' - proj_word - (match andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z as b return b = true -> b = true with - | true => fun _ => eq_refl - | false => fun x => x - end word_bounded). -Lemma word_to_unbounded_helper {x e : nat} : (x < pow2 e)%nat -> (Z.of_nat e <= Z.of_nat bit_width)%Z -> ((0 <=? word64ToZ (ZToWord64 (Z.of_nat x))) && (word64ToZ (ZToWord64 (Z.of_nat x)) <=? 2 ^ (Z.of_nat e) - 1))%bool = true. -Proof. - rewrite pow2_id; intro H; apply Nat2Z.inj_lt in H; revert H. - rewrite Z.pow_Zpow; simpl Z.of_nat. - intros H H'. - assert (2^Z.of_nat e <= 2^Z.of_nat bit_width) by auto with zarith. - rewrite ?word64ToZ_ZToWord64 by omega. - match goal with - | [ |- context[andb ?x ?y] ] - => destruct x eqn:?, y eqn:?; try reflexivity; Z.ltb_to_lt - end; - intros; omega. -Qed. -Definition word_to_unbounded_word {sz} (x : word sz) : (Z.of_nat sz <=? Z.of_nat bit_width)%Z = true -> unbounded_word (Z.of_nat sz). -Proof. - refine (fun pf => Build_bounded_word (Z.of_N (wordToN x)) _). - abstract (rewrite wordToN_nat, nat_N_Z; Z.ltb_to_lt; apply (word_to_unbounded_helper (wordToNat_bound x)); simpl; omega). -Defined. -Definition word32_to_unbounded_word (x : word 32) : unbounded_word 32. -Proof. apply (word_to_unbounded_word x); reflexivity. Defined. -Definition word31_to_unbounded_word (x : word 31) : unbounded_word 31. -Proof. apply (word_to_unbounded_word x); reflexivity. Defined. - -Local Opaque word64. -Declare Reduction app_tuple_map := cbv [app_wire_digitsW app_fe5211_32W app_fe5211_32 HList.mapt HList.mapt' Tuple.map on_tuple List.map List.app length_fe5211_32 List.length wire_widths Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' fst snd]. -Definition fe5211_32WToZ (x : fe5211_32W) : SpecificGen.GF5211_32.fe5211_32 - := Eval app_tuple_map in - app_fe5211_32W x (Tuple.map (fun v : word64 => v : Z)). -Definition fe5211_32ZToW (x : SpecificGen.GF5211_32.fe5211_32) : fe5211_32W - := Eval app_tuple_map in - app_fe5211_32W x (Tuple.map (fun v : Z => v : word64)). -Definition wire_digitsWToZ (x : wire_digitsW) : SpecificGen.GF5211_32.wire_digits - := Eval app_tuple_map in - app_wire_digitsW x (Tuple.map (fun v : word64 => v : Z)). -Definition wire_digitsZToW (x : SpecificGen.GF5211_32.wire_digits) : wire_digitsW - := Eval app_tuple_map in - app_wire_digitsW x (Tuple.map (fun v : Z => v : word64)). -Definition fe5211_32W_word64ize (x : fe5211_32W) : fe5211_32W - := Eval app_tuple_map in - app_fe5211_32W x (Tuple.map word64ize). -Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW - := Eval app_tuple_map in - app_wire_digitsW x (Tuple.map word64ize). - -(** TODO: Turn this into a lemma to speed up proofs *) -Ltac unfold_is_bounded_in' H := - lazymatch type of H with - | andb _ _ = true - => apply andb_prop in H; - let H1 := fresh in - let H2 := fresh in - destruct H as [H1 H2]; - unfold_is_bounded_in' H1; - unfold_is_bounded_in' H2 - | _ => idtac - end. -Ltac preunfold_is_bounded_in H := - unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe5211_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 Tuple.map List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths HList.hlistP HList.hlistP' Tuple.on_tuple] in H. -Ltac unfold_is_bounded_in H := - preunfold_is_bounded_in H; - unfold_is_bounded_in' H. - -Ltac preunfold_is_bounded := - unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe5211_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 Tuple.map List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths HList.hlistP HList.hlistP' Tuple.on_tuple]. - -Ltac unfold_is_bounded := - preunfold_is_bounded; - repeat match goal with - | [ |- andb _ _ = true ] => apply andb_true_intro - | [ |- and _ _ ] => split - end. - -Local Transparent bit_width. -Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width. -Definition unfold_Pow2_64 : 2^Z.of_nat bit_width = Pow2_64 := eq_refl. -Local Opaque bit_width. - -Local Ltac prove_lt_bit_width := - rewrite unfold_Pow2_64; cbv [Pow2_64]; omega. - -Lemma fe5211_32ZToW_WToZ (x : fe5211_32W) : fe5211_32ZToW (fe5211_32WToZ x) = x. -Proof. - hnf in x; destruct_head' prod; cbv [fe5211_32WToZ fe5211_32ZToW]. - rewrite !ZToWord64_word64ToZ; reflexivity. -Qed. - -Lemma fe5211_32WToZ_ZToW x : is_bounded x = true -> fe5211_32WToZ (fe5211_32ZToW x) = x. -Proof. - hnf in x; destruct_head' prod; cbv [fe5211_32WToZ fe5211_32ZToW]. - intro H. - unfold_is_bounded_in H; destruct_head' and. - Z.ltb_to_lt. - rewrite !word64ToZ_ZToWord64 by prove_lt_bit_width. - reflexivity. -Qed. - -Lemma fe5211_32W_word64ize_id x : fe5211_32W_word64ize x = x. -Proof. - hnf in x; destruct_head' prod. - cbv [fe5211_32W_word64ize]; - repeat apply f_equal2; apply word64ize_id. -Qed. -Lemma wire_digitsW_word64ize_id x : wire_digitsW_word64ize x = x. -Proof. - hnf in x; destruct_head' prod. - cbv [wire_digitsW_word64ize]; - repeat apply f_equal2; apply word64ize_id. -Qed. - -Definition uncurry_unop_fe5211_32W {T} (op : fe5211_32W -> T) - := Eval cbv (*-[word64]*) in Tuple.uncurry (n:=length_fe5211_32) op. -Definition curry_unop_fe5211_32W {T} op : fe5211_32W -> T - := Eval cbv (*-[word64]*) in fun f => app_fe5211_32W f (Tuple.curry (n:=length_fe5211_32) op). -Definition uncurry_binop_fe5211_32W {T} (op : fe5211_32W -> fe5211_32W -> T) - := Eval cbv (*-[word64]*) in uncurry_unop_fe5211_32W (fun f => uncurry_unop_fe5211_32W (op f)). -Definition curry_binop_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> T - := Eval cbv (*-[word64]*) in appify2 (fun f => curry_unop_fe5211_32W (curry_unop_fe5211_32W op f)). - -Definition uncurry_unop_wire_digitsW {T} (op : wire_digitsW -> T) - := Eval cbv (*-[word64]*) in Tuple.uncurry (n:=length wire_widths) op. -Definition curry_unop_wire_digitsW {T} op : wire_digitsW -> T - := Eval cbv (*-[word64]*) in fun f => app_wire_digitsW f (Tuple.curry (n:=length wire_widths) op). - -Definition uncurry_9op_fe5211_32W {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe5211_32W (fun x0 => - uncurry_unop_fe5211_32W (fun x1 => - uncurry_unop_fe5211_32W (fun x2 => - uncurry_unop_fe5211_32W (fun x3 => - uncurry_unop_fe5211_32W (fun x4 => - uncurry_unop_fe5211_32W (fun x5 => - uncurry_unop_fe5211_32W (fun x6 => - uncurry_unop_fe5211_32W (fun x7 => - uncurry_unop_fe5211_32W (fun x8 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))). -Definition curry_9op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T - := Eval cbv (*-[word64]*) in - appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 - => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8). - -Definition proj1_fe5211_32W (x : fe5211_32) : fe5211_32W - := Eval app_tuple_map in - app_fe5211_32 x (HList.mapt (fun _ => (@proj_word _ _))). -Coercion proj1_fe5211_32 (x : fe5211_32) : SpecificGen.GF5211_32.fe5211_32 - := fe5211_32WToZ (proj1_fe5211_32W x). - -Lemma is_bounded_proj1_fe5211_32 (x : fe5211_32) : is_bounded (proj1_fe5211_32 x) = true. -Proof. - revert x; refine (app_fe5211_32_dep _); intro x. - hnf in x; destruct_head' prod; destruct_head' bounded_word. - cbv [is_bounded proj1_fe5211_32 proj1_fe5211_32W fe5211_32WToZ to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word length_fe5211_32 is_bounded_gen]. - apply fold_right_andb_true_iff_fold_right_and_True. - cbv [fold_right List.map]. - cbv beta in *. - repeat split; auto using project_is_boundedT. -Qed. - -Definition proj1_wire_digitsW (x : wire_digits) : wire_digitsW - := app_wire_digits x (HList.mapt (fun _ => proj_word)). -Coercion proj1_wire_digits (x : wire_digits) : SpecificGen.GF5211_32.wire_digits - := wire_digitsWToZ (proj1_wire_digitsW x). - -Lemma is_bounded_proj1_wire_digits (x : wire_digits) : wire_digits_is_bounded (proj1_wire_digits x) = true. -Proof. - revert x; refine (app_wire_digits_dep _); intro x. - hnf in x; destruct_head' prod; destruct_head' bounded_word. - cbv [wire_digits_is_bounded proj1_wire_digits proj1_wire_digitsW wire_digitsWToZ to_list length wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word is_bounded_gen wire_widths HList.mapt HList.mapt' app_wire_digits fst snd]. - apply fold_right_andb_true_iff_fold_right_and_True. - cbv [fold_right List.map]. - cbv beta in *. - repeat split; auto using project_is_boundedT. -Qed. - -Local Ltac make_exist_W' x app_W_dep := - let H := fresh in - revert x; refine (@app_W_dep _ _ _); intros x H; - let x' := fresh in - set (x' := x); - cbv [tuple tuple' length_fe5211_32 List.length wire_widths] in x; - destruct_head' prod; - let rec do_refine v H := - first [ let v' := (eval cbv [snd fst] in (snd v)) in - refine (_, Build_bounded_word v' _); - [ do_refine (fst v) (proj2 H) | subst x'; abstract exact (proj1 H) ] - | let v' := (eval cbv [snd fst] in v) in - refine (Build_bounded_word v' _); subst x'; abstract exact (proj1 H) ] in - let H' := constr:(proj1 (@fold_right_andb_true_iff_fold_right_and_True _) H) in - let T := type of H' in - let T := (eval cbv [id - List.fold_right List.map List.length List.app ListUtil.map2 List.rev - Tuple.to_list Tuple.to_list' Tuple.from_list Tuple.from_list' Tuple.map2 Tuple.on_tuple2 - fe5211_32 bounds fe5211_32WToZ length_fe5211_32 - wire_digits wire_digit_bounds wire_digitsWToZ wire_widths] in T) in - let H' := constr:(H' : T) in - let v := (eval unfold x' in x') in - do_refine v H'. -Local Ltac make_exist'' x exist_W ZToW := - let H := fresh in - intro H; apply (exist_W (ZToW x)); - abstract ( - hnf in x; destruct_head' prod; - let H' := fresh in - pose proof H as H'; - unfold_is_bounded_in H; - destruct_head' and; simpl in *; - Z.ltb_to_lt; - rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width; - assumption - ). -Local Ltac make_exist' x app_W_dep exist'' exist_W ZToW := - let H := fresh in - revert x; refine (@app_W_dep _ _ _); intros x H; - let x' := fresh in - set (x' := x) in *; - cbv [tuple tuple' length_fe5211_32 List.length wire_widths] in x; - destruct_head' prod; - let rec do_refine v := - first [ let v' := (eval cbv [exist_W ZToW exist'' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word v)) in - refine (Build_bounded_word v' _); subst x'; abstract exact (word_bounded v) - | let v' := (eval cbv [exist_W ZToW exist'' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word (snd v))) in - refine (_, Build_bounded_word v' _); - [ do_refine (fst v) | subst x'; abstract exact (word_bounded (snd v)) ] ] in - let v := (eval unfold x' in (exist'' x' H)) in - do_refine v. - -Definition exist_fe5211_32W' (x : fe5211_32W) : is_bounded (fe5211_32WToZ x) = true -> fe5211_32. -Proof. make_exist_W' x (@app_fe5211_32W_dep). Defined. -Definition exist_fe5211_32W (x : fe5211_32W) : is_bounded (fe5211_32WToZ x) = true -> fe5211_32 - := Eval cbv [app_fe5211_32W_dep exist_fe5211_32W' fe5211_32ZToW] in exist_fe5211_32W' x. -Definition exist_fe5211_32'' (x : SpecificGen.GF5211_32.fe5211_32) : is_bounded x = true -> fe5211_32. -Proof. make_exist'' x exist_fe5211_32W fe5211_32ZToW. Defined. -Definition exist_fe5211_32' (x : SpecificGen.GF5211_32.fe5211_32) : is_bounded x = true -> fe5211_32. -Proof. make_exist' x (@app_fe5211_32W_dep) exist_fe5211_32'' exist_fe5211_32W fe5211_32ZToW. Defined. -Definition exist_fe5211_32 (x : SpecificGen.GF5211_32.fe5211_32) : is_bounded x = true -> fe5211_32 - := Eval cbv [exist_fe5211_32' exist_fe5211_32W exist_fe5211_32' app_fe5211_32 app_fe5211_32W_dep] in - exist_fe5211_32' x. - -Lemma proj1_fe5211_32_exist_fe5211_32W x pf : proj1_fe5211_32 (exist_fe5211_32W x pf) = fe5211_32WToZ x. -Proof. now hnf in x; destruct_head' prod. Qed. -Lemma proj1_fe5211_32W_exist_fe5211_32 x pf : proj1_fe5211_32W (exist_fe5211_32 x pf) = fe5211_32ZToW x. -Proof. now hnf in x; destruct_head' prod. Qed. -Lemma proj1_fe5211_32_exist_fe5211_32 x pf : proj1_fe5211_32 (exist_fe5211_32 x pf) = x. -Proof. - hnf in x; destruct_head' prod. - cbv [proj1_fe5211_32 exist_fe5211_32 proj1_fe5211_32W fe5211_32WToZ proj_word Build_bounded_word Build_bounded_word']. - unfold_is_bounded_in pf. - destruct_head' and. - Z.ltb_to_lt. - rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width. - reflexivity. -Qed. - -Definition exist_wire_digitsW' (x : wire_digitsW) - : wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits. -Proof. make_exist_W' x (@app_wire_digitsW_dep). Defined. -Definition exist_wire_digitsW (x : wire_digitsW) - : wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits - := Eval cbv [app_wire_digitsW_dep exist_wire_digitsW' wire_digitsZToW] in exist_wire_digitsW' x. -Definition exist_wire_digits'' (x : SpecificGen.GF5211_32.wire_digits) - : wire_digits_is_bounded x = true -> wire_digits. -Proof. make_exist'' x exist_wire_digitsW wire_digitsZToW. Defined. -Definition exist_wire_digits' (x : SpecificGen.GF5211_32.wire_digits) - : wire_digits_is_bounded x = true -> wire_digits. -Proof. make_exist' x (@app_wire_digitsW_dep) exist_wire_digits'' exist_wire_digitsW wire_digitsZToW. Defined. -Definition exist_wire_digits (x : SpecificGen.GF5211_32.wire_digits) - : wire_digits_is_bounded x = true -> wire_digits - := Eval cbv [exist_wire_digits' exist_wire_digitsW exist_wire_digits' app_wire_digits app_wire_digitsW_dep] in - exist_wire_digits' x. - -Lemma proj1_wire_digits_exist_wire_digitsW x pf : proj1_wire_digits (exist_wire_digitsW x pf) = wire_digitsWToZ x. -Proof. now hnf in x; destruct_head' prod. Qed. -Lemma proj1_wire_digitsW_exist_wire_digits x pf : proj1_wire_digitsW (exist_wire_digits x pf) = wire_digitsZToW x. -Proof. now hnf in x; destruct_head' prod. Qed. -Lemma proj1_wire_digits_exist_wire_digits x pf : proj1_wire_digits (exist_wire_digits x pf) = x. -Proof. - hnf in x; destruct_head' prod. - cbv [proj1_wire_digits exist_wire_digits proj1_wire_digitsW wire_digitsWToZ proj_word Build_bounded_word Build_bounded_word' app_wire_digits HList.mapt HList.mapt' length wire_widths fst snd]. - unfold_is_bounded_in pf. - destruct_head' and. - Z.ltb_to_lt. - rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width. - reflexivity. -Qed. - -Module opt. - Definition word64ToZ := Eval vm_compute in word64ToZ. - Definition word64ToN := Eval vm_compute in @wordToN bit_width. - Definition NToWord64 := Eval vm_compute in NToWord64. - Definition bit_width := Eval vm_compute in bit_width. - Definition Zleb := Eval cbv [Z.leb] in Z.leb. - Definition andb := Eval vm_compute in andb. - Definition word64ize := Eval vm_compute in word64ize. -End opt. - -Local Transparent bit_width. -Local Ltac do_change lem := - match lem with - | context L[andb (?x <=? ?y)%Z (?y <=? ?z)] - => let x' := (eval vm_compute in x) in - let z' := (eval vm_compute in z) in - lazymatch y with - | word64ToZ (word64ize ?v) - => let y' := constr:(opt.word64ToZ (opt.word64ize v)) in - let L' := context L[andb (opt.Zleb x' y') (opt.Zleb y' z')] in - do_change L' - end - | _ => lem - end. -Definition fe5211_32_word64ize (x : fe5211_32) : fe5211_32. -Proof. - set (x' := x). - hnf in x; destruct_head' prod. - let lem := constr:(exist_fe5211_32W (fe5211_32W_word64ize (proj1_fe5211_32W x'))) in - let lem := (eval cbv [proj1_fe5211_32W x' fe5211_32W_word64ize proj_word exist_fe5211_32W Build_bounded_word' Build_bounded_word] in lem) in - let lem := do_change lem in - refine (lem _); - change (is_bounded (fe5211_32WToZ (fe5211_32W_word64ize (proj1_fe5211_32W x'))) = true); - abstract (rewrite fe5211_32W_word64ize_id; apply is_bounded_proj1_fe5211_32). -Defined. -Definition wire_digits_word64ize (x : wire_digits) : wire_digits. -Proof. - set (x' := x). - hnf in x; destruct_head' prod. - let lem := constr:(exist_wire_digitsW (wire_digitsW_word64ize (proj1_wire_digitsW x'))) in - let lem := (eval cbv [proj1_wire_digitsW x' wire_digitsW_word64ize proj_word exist_wire_digitsW Build_bounded_word Build_bounded_word'] in lem) in - let lem := do_change lem in - let lem := (eval cbv [word64ize opt.word64ize andb Z.leb Z.compare CompOpp Pos.compare] in lem) in - refine (lem _); - change (wire_digits_is_bounded (wire_digitsWToZ (wire_digitsW_word64ize (proj1_wire_digitsW x'))) = true); - abstract (rewrite wire_digitsW_word64ize_id; apply is_bounded_proj1_wire_digits). -Defined. - -Lemma is_bounded_to_nth_default x (H : is_bounded x = true) - : forall n : nat, - (n < length limb_widths)%nat - -> (0 <= nth_default 0 (Tuple.to_list length_fe5211_32 x) n <= - snd (b_of (nth_default (-1) limb_widths n)))%Z. -Proof. - hnf in x; destruct_head' prod. - unfold_is_bounded_in H; destruct_head' and. - Z.ltb_to_lt. - unfold nth_default; simpl. - intros. - repeat match goal with - | [ |- context[nth_error _ ?x] ] - => is_var x; destruct x; simpl - end; - omega. -Qed. - -(* END precomputation *) - -(* Precompute constants *) - -Definition one' := Eval vm_compute in exist_fe5211_32 SpecificGen.GF5211_32.one_ eq_refl. -Definition one := Eval cbv [one' fe5211_32_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe5211_32_word64ize one'. - -Definition zero' := Eval vm_compute in exist_fe5211_32 SpecificGen.GF5211_32.zero_ eq_refl. -Definition zero := Eval cbv [zero' fe5211_32_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe5211_32_word64ize zero'. - -Lemma fold_chain_opt_gen {A B} (F : A -> B) is_bounded ls id' op' id op chain - (Hid_bounded : is_bounded (F id') = true) - (Hid : id = F id') - (Hop_bounded : forall x y, is_bounded (F x) = true - -> is_bounded (F y) = true - -> is_bounded (op (F x) (F y)) = true) - (Hop : forall x y, is_bounded (F x) = true - -> is_bounded (F y) = true - -> op (F x) (F y) = F (op' x y)) - (Hls_bounded : forall n, is_bounded (F (nth_default id' ls n)) = true) - : F (fold_chain_opt id' op' chain ls) - = fold_chain_opt id op chain (List.map F ls) - /\ is_bounded (F (fold_chain_opt id' op' chain ls)) = true. -Proof. - rewrite !fold_chain_opt_correct. - revert dependent ls; induction chain as [|x xs IHxs]; intros. - { pose proof (Hls_bounded 0%nat). - destruct ls; simpl; split; trivial; congruence. } - { destruct x; simpl; unfold Let_In; simpl. - rewrite (fun ls pf => proj1 (IHxs ls pf)) at 1; simpl. - { do 2 f_equal. - rewrite <- Hop, Hid by auto. - rewrite !map_nth_default_always. - split; try reflexivity. - apply (IHxs (_::_)). - intros [|?]; autorewrite with simpl_nth_default; auto. - rewrite <- Hop; auto. } - { intros [|?]; simpl; - autorewrite with simpl_nth_default; auto. - rewrite <- Hop; auto. } } -Qed. - -Lemma encode_bounded x : is_bounded (encode x) = true. -Proof. - pose proof (bounded_encode x). - generalize dependent (encode x). - intro t; compute in t; intros. - destruct_head' prod. - unfold Pow2Base.bounded in H. - cbv [nth_default Tuple.to_list Tuple.to_list' List.length limb_widths params5211_32] in H. - repeat match type of H with - | context[nth_error (cons _ _) _] - => let H' := fresh in - pose proof (H O) as H'; specialize (fun i => H (S i)); simpl @nth_error in H, H'; - cbv beta iota in H' - end. - clear H. - simpl in *. - cbv [Z.pow_pos Z.mul Pos.mul Pos.iter nth_default nth_error value] in *. - unfold is_bounded. - apply fold_right_andb_true_iff_fold_right_and_True. - cbv [is_bounded proj1_fe5211_32 to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word fold_right length_fe5211_32]. - repeat split; rewrite !Bool.andb_true_iff, !Z.leb_le; omega. -Qed. - -Definition encode (x : F modulus) : fe5211_32 - := exist_fe5211_32 (encode x) (encode_bounded x). - -Definition decode (x : fe5211_32) : F modulus - := ModularBaseSystem.decode (proj1_fe5211_32 x). - -Lemma proj1_fe5211_32_encode x - : proj1_fe5211_32 (encode x) = ModularBaseSystem.encode x. -Proof. - cbv [encode]. - generalize (encode_bounded x); generalize (ModularBaseSystem.encode x). - intros y pf; intros; hnf in y; destruct_head_hnf' prod. - cbv [proj1_fe5211_32 exist_fe5211_32 proj1_fe5211_32W Build_bounded_word Build_bounded_word' fe5211_32WToZ proj_word]. - unfold_is_bounded_in pf. - destruct_head' and. - Z.ltb_to_lt. - rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width. - reflexivity. -Qed. - -Lemma decode_exist_fe5211_32 x pf - : decode (exist_fe5211_32 x pf) = ModularBaseSystem.decode x. -Proof. - hnf in x; destruct_head' prod. - cbv [decode proj1_fe5211_32 exist_fe5211_32 proj1_fe5211_32W Build_bounded_word Build_bounded_word' fe5211_32WToZ proj_word]. - unfold_is_bounded_in pf. - destruct_head' and. - Z.ltb_to_lt. - rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width. - reflexivity. -Qed. - -Definition div (f g : fe5211_32) : fe5211_32 - := exist_fe5211_32 (div (proj1_fe5211_32 f) (proj1_fe5211_32 g)) (encode_bounded _). - -Definition eq (f g : fe5211_32) : Prop := eq (proj1_fe5211_32 f) (proj1_fe5211_32 g). - - -Notation in_op_correct_and_bounded k irop op - := (((Tuple.map (n:=k) fe5211_32WToZ irop = op) - /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ irop))%type) - (only parsing). - -(*Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat) - : forall (irop : Tower.tower_nd fe5211_32W (Tuple.tuple fe5211_32W count_out) count_in) - (op : Tower.tower_nd GF5211_32.fe5211_32 (Tuple.tuple GF5211_32.fe5211_32 count_out) count_in) - (cont : Prop -> Prop), - Prop - := match count_in return - forall (irop : Tower.tower_nd fe5211_32W (Tuple.tuple fe5211_32W count_out) count_in) - (op : Tower.tower_nd GF5211_32.fe5211_32 (Tuple.tuple GF5211_32.fe5211_32 count_out) count_in) - (cont : Prop -> Prop), - Prop - with - | O => fun irop op cont => cont (in_op_correct_and_bounded count_out irop op) - | S n => fun irop op cont - => forall x : fe5211_32W, - @inm_op_correct_and_bounded' - n count_out (irop x) (op (fe5211_32WToZ x)) - (fun P => cont (is_bounded (fe5211_32WToZ x) = true -> P)) - end. -Definition inm_op_correct_and_bounded count_in count_out irop op - := Eval cbv [inm_op_correct_and_bounded' Tower.tower_nd Tuple.tuple Tuple.tuple' HList.hlistP HList.hlistP'] in - inm_op_correct_and_bounded' count_in count_out irop op (fun P => P). -Fixpoint inm_op_correct_and_bounded_prefix' (count_in count_out : nat) - : forall (irop : Tower.tower_nd fe5211_32W (Tuple.tuple fe5211_32W count_out) count_in) - (op : Tower.tower_nd GF5211_32.fe5211_32 (Tuple.tuple GF5211_32.fe5211_32 count_out) count_in), - Prop - := match count_in return - forall (irop : Tower.tower_nd fe5211_32W (Tuple.tuple fe5211_32W count_out) count_in) - (op : Tower.tower_nd GF5211_32.fe5211_32 (Tuple.tuple GF5211_32.fe5211_32 count_out) count_in), - Prop - with - | O => fun irop op => in_op_correct_and_bounded count_out irop op - | S n => fun irop op - => forall x : fe5211_32W, - is_bounded (fe5211_32WToZ x) = true - -> @inm_op_correct_and_bounded_prefix' - n count_out (irop x) (op (fe5211_32WToZ x)) - end. -Definition inm_op_correct_and_bounded_prefix count_in count_out irop op - := inm_op_correct_and_bounded_prefix' count_in count_out irop op. - -Lemma inm_op_correct_and_bounded_iff_prefix' count_in count_out irop op - (cont : Prop -> Prop) - (cont_forall : forall T (P : T -> Prop), cont (forall x : T, P x) <-> forall x : T, cont (P x)) - : inm_op_correct_and_bounded' count_in count_out irop op cont <-> cont (inm_op_correct_and_bounded_prefix' count_in count_out irop op). -Proof. - revert dependent cont; induction count_in as [|count_in IHcount_in]; intros. - { reflexivity. } - { simpl. - rewrite cont_forall. - split; intros H' x; specialize (H' x); - specialize (IHcount_in (irop x) (op (fe5211_32WToZ x)) (fun P => cont (is_bounded (fe5211_32WToZ x) = true -> P))); - cbv beta in *; - [ erewrite <- IHcount_in; [ assumption | .. ] - | erewrite -> IHcount_in; [ assumption | .. ] ]; - clear IHcount_in. - { intros; repeat setoid_rewrite cont_forall; split; eauto. } - { intros; repeat setoid_rewrite cont_forall; split; eauto. } } -Qed. - -Lemma inm_op_correct_and_bounded_iff_prefix count_in count_out irop op - : inm_op_correct_and_bounded count_in count_out irop op <-> inm_op_correct_and_bounded_prefix count_in count_out irop op. -Proof. - apply (inm_op_correct_and_bounded_iff_prefix' count_in count_out irop op (fun P => P)). - reflexivity. -Qed. - -Definition inm_op_correct_and_bounded1 count_in irop op - := Eval cbv [inm_op_correct_and_bounded Tuple.map Tuple.to_list Tuple.to_list' Tuple.from_list Tuple.from_list' Tuple.on_tuple List.map] in - inm_op_correct_and_bounded count_in 1 irop op.*) -Notation inm_op_correct_and_bounded n m irop op - := ((forall x, - HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=n%nat%type) fe5211_32WToZ x) - -> in_op_correct_and_bounded m (irop x) (op (Tuple.map (n:=n) fe5211_32WToZ x)))) - (only parsing). -Notation ibinop_correct_and_bounded irop op := (inm_op_correct_and_bounded 2 1 irop op) (only parsing). -Notation iunop_correct_and_bounded irop op := (inm_op_correct_and_bounded 1 1 irop op) (only parsing). -Notation iunop_FEToZ_correct irop op - := (forall x, - is_bounded (fe5211_32WToZ x) = true - -> word64ToZ (irop x) = op (fe5211_32WToZ x)) (only parsing). -Notation iunop_FEToWire_correct_and_bounded irop op - := (forall x, - is_bounded (fe5211_32WToZ x) = true - -> wire_digitsWToZ (irop x) = op (fe5211_32WToZ x) - /\ wire_digits_is_bounded (wire_digitsWToZ (irop x)) = true) (only parsing). -Notation iunop_WireToFE_correct_and_bounded irop op - := (forall x, - wire_digits_is_bounded (wire_digitsWToZ x) = true - -> fe5211_32WToZ (irop x) = op (wire_digitsWToZ x) - /\ is_bounded (fe5211_32WToZ (irop x)) = true) (only parsing). -Notation i9top_correct_and_bounded k irop op := (inm_op_correct_and_bounded 9 k irop op) (only parsing). - -Notation prefreeze := GF5211_32.prefreeze. |