diff options
| -rw-r--r-- | _CoqProject | 6 | ||||
| -rw-r--r-- | cleanup.md | 139 | ||||
| -rw-r--r-- | src/BoundedArithmetic/CaseUtil.v | 18 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Eta.v | 70 | ||||
| -rw-r--r-- | src/BoundedArithmetic/StripCF.v | 74 | ||||
| -rw-r--r-- | src/Experiments/Ed25519_imports.hs | 5 | ||||
| -rw-r--r-- | src/Experiments/ExtrHaskellNats.v | 111 | ||||
| -rw-r--r-- | src/Experiments/GenericFieldPow.v | 350 | ||||
| -rw-r--r-- | src/Experiments/c.sh | 19 | ||||
| -rw-r--r-- | src/Specific/SC25519.v | 171 | ||||
| -rw-r--r-- | src/SpecificGen/GFtemplate3mod4 | 773 | ||||
| -rw-r--r-- | src/SpecificGen/GFtemplate5mod8 | 782 | ||||
| -rw-r--r-- | src/SpecificGen/README.md | 5 | ||||
| -rwxr-xr-x | src/SpecificGen/copy_bounds.sh | 29 | ||||
| -rw-r--r-- | src/SpecificGen/fill_template.py | 39 |
15 files changed, 0 insertions, 2591 deletions
diff --git a/_CoqProject b/_CoqProject index d545cc6b2..823fda21b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -23,13 +23,10 @@ src/BoundedArithmetic/ArchitectureToZLike.v src/BoundedArithmetic/ArchitectureToZLikeProofs.v src/BoundedArithmetic/BaseSystem.v src/BoundedArithmetic/BaseSystemProofs.v -src/BoundedArithmetic/CaseUtil.v -src/BoundedArithmetic/Eta.v src/BoundedArithmetic/Interface.v src/BoundedArithmetic/InterfaceProofs.v src/BoundedArithmetic/Pow2Base.v src/BoundedArithmetic/Pow2BaseProofs.v -src/BoundedArithmetic/StripCF.v src/BoundedArithmetic/Double/Core.v src/BoundedArithmetic/Double/Proofs/BitwiseOr.v src/BoundedArithmetic/Double/Proofs/Decode.v @@ -46,8 +43,6 @@ src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/EdwardsMontgomery.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v -src/Experiments/ExtrHaskellNats.v -src/Experiments/GenericFieldPow.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v @@ -190,7 +185,6 @@ src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Specific/IntegrationTest.v src/Specific/NewBaseSystemTest.v -src/Specific/SC25519.v src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v diff --git a/cleanup.md b/cleanup.md deleted file mode 100644 index b26db1cab..000000000 --- a/cleanup.md +++ /dev/null @@ -1,139 +0,0 @@ -# Fiat-Crypto Cleanup - -The primary objectives here are to reduce the substantial amount of code-bloat -that fiat-crypto has accrued, and to use the lessons we've learned so far to -rewrite some parts of the library in ways that will cause us less future pain. -These changes will both make our own lives easier and make the library more -approachable to others. - -## Overview - -- Field Arithmetic Implementation (Base System): Rewrite using a new, less awkward representation (in progress). -- Elliptic Curves : Use dependently-typed division and enhance super-`nsatz` -- Spec : Remove the stuff that does not belong in spec. -- Algebra/Prime Field libraries : Possibly introduce more bundling. -- Experiments/Ed25519 : Move the "spaghetti code" to the various parts of the library where it belongs. -- Util : Keep pretty much as-is, even if many lemmas are not used after rewrites. -- Compilery Bits : Reorganize and spend some time thinking about design. -- PointEncoding : Significant refactor, make interfaces line up and remove duplicated or redundant code. -- Specific/SpecificGen : Make a more general and nicely-presented catalog of examples for people to look at and be impressed by. - -## Field Arithmetic Implementation - -Originally, we represented field-element bignums using two lists, one -representing the constant weights (e.g. `[1, 2^26, 2^51,...] or [26, 25, -26,...]) and one with the variable runtime values. The new representation -couples the weights and the runtime values, (e.g `[(1, x0), (2^51, x1), (2^51, -x2), (2^26, x1)]`). - -This approach has several advantages, but the most important of these is that -the basic arithmetic operations have gotten much simpler. Here is the old -version of `mul`: - -``` - (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *) - Fixpoint mul_bi' (i:nat) (vsr:digits) := - match vsr with - | v::vsr' => v * crosscoef i (length vsr') :: mul_bi' i vsr' - | nil => nil - end. - Definition mul_bi (i:nat) (vs:digits) : digits := - zeros i ++ rev (mul_bi' i (rev vs)). - - (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) - Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => - mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs - | _ => nil - end. - Definition mul us := mul' (rev us). -``` - -This version doesn't even include a few hundred lines of proof needed to prove -that `mul` is correct or 150 lines of extra work in ModularBaseSystemOpt.v to -mark runtime operations. Here is the new `mul` and its proof: - -``` - Definition mul (p q:list limb) : list limb := - List.flat_map (fun t => List.map (fun t' => (fst t * fst t', (snd t * snd t')%RT)) q) p. - - Lemma eval_map_mul a x q : eval (List.map (fun t => (a * fst t, x * snd t)) q) = a * x * eval q. - Proof. induction q; simpl List.map; autorewrite with push_eval cancel_pair; nsatz. Qed. - - Lemma eval_mul p q : eval (mul p q) = eval p * eval q. - Proof. induction p; simpl mul; autorewrite with push_eval cancel_pair; try nsatz. Qed. -``` - -The "RT" notation marks runtime operations, so there's no need for an extra step. - -Besides shaving some orders of magnitude off of implementation effort, size, -and compile time, we also no longer need to carry around preconditions that -discuss the correspondence between the weights list and the runtime list (for -instance, that they have the same length). - -## Elliptic Curves - -1. Division should be modified to use a dependent type for the denominator, - which carries a proof that the denominator is nonzero. This removes some -ugliness (for instance, with proving homomorphisms, where it is necessary to -show that both divisions do similar things for all possible inputs. Division by -zero is undefined, so if zero is a possible input, this is challenging.) Also, -simply making it impossible to divide by zero more accurately matches how we -think of division. -2. Improve super-`nsatz` as described in Andres and Jason's Coq enhancements - proposal. - -## Spec - -There's a bunch of clutter scattered across the files that either doesn't -belong in spec or could be expressed better. If someone went through all the -files and thought carefully about them, it would be time well spent. - -Additionally, the things in Encoding.v and ModularWordEncoding.v will likely go -away during the PointEncoding cleanup. - -## Algebra/Prime Field Libraries - -Mostly leave as-is, these are great examples of parts of fiat-crypto that are -currently nice, probably because they are fairly well-defined sections that -were designed all at once with the big picture in mind, instead of being -incrementally assembled and revised. We might want to consider bundling some of -the algebraic structures. - -## Experiments/Ed25519.v - -This file was assembled as we scrambled to meet the PLDI deadline and contains -mostly "glue" that makes different interfaces across fiat-crypto actually line -up with each other. We should have someone go through it and relocate that sort -of code to where it actually belongs, and/or make the necessary changes to -interfaces. - -## Util - -We should keep the Util files (especially the big ones like ZUtil and ListUtil) -mostly as-is, although once the old BaseSystem goes away most of the lemmas -won't be used by fiat-crypto. If compile time becomes a problem, we might want -to factor out the unused lemmas and store them separately, but we should not -get rid of anything that could be a candidate for Coq's standard library. - -## Compilery Bits - -We should reorganize the compilery files (meaning bounds-checking, PHOAS, etc.) -to be more comprehensible to people who are not Jason. We should also remove -unnecessary code (are we ever going to use the code under the Assembly -directory?) and do another "think hard about whether these pieces are designed -well" session. - -## PointEncoding - -These files are a mix of very very old code and code that was thrown in to make -things work right before the PLDI deadline. It just needs to have redundant -code removed and proof structures improved. - - -## Specific/SpecificGen - -As we are transitioning from this being a research prototype to it being a Real -Thing People Might Look At, we might want to consider making a more presentable -and cohesive catalog of examples than we currently have. diff --git a/src/BoundedArithmetic/CaseUtil.v b/src/BoundedArithmetic/CaseUtil.v deleted file mode 100644 index 2d1ab6c58..000000000 --- a/src/BoundedArithmetic/CaseUtil.v +++ /dev/null @@ -1,18 +0,0 @@ -Require Import Coq.Arith.Arith Coq.Arith.Max. - -Ltac case_max := - match goal with [ |- context[max ?x ?y] ] => - destruct (le_dec x y); - match goal with - | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_r by - (exact H) - | [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_l by - (exact (le_Sn_le _ _ (not_le _ _ H))) - end - end. - -Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A) - : (if b then f x else g x) = (if b then f else g) x. -Proof. - destruct b; reflexivity. -Qed. diff --git a/src/BoundedArithmetic/Eta.v b/src/BoundedArithmetic/Eta.v deleted file mode 100644 index b48b8cff1..000000000 --- a/src/BoundedArithmetic/Eta.v +++ /dev/null @@ -1,70 +0,0 @@ -(** * Bounded arithmetic η expansion *) -(** This is useful for allowing us to refold the projections. *) -Require Import Crypto.BoundedArithmetic.Interface. - -Definition eta_decode {n W} (x : decoder n W) : decoder n W := {| decode := decode |}. -Section InstructionGallery. - Context {n W} {Wdecoder : decoder n W}. - Definition eta_ldi (x : load_immediate W) := {| ldi := ldi |}. - Definition eta_shrd (x : shift_right_doubleword_immediate W) := {| shrd := shrd |}. - Definition eta_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf := shrdf |}. - Definition eta_shl (x : shift_left_immediate W) := {| shl := shl |}. - Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf := shlf |}. - Definition eta_shr (x : shift_right_immediate W) := {| shr := shr |}. - Definition eta_shrf (x : shift_right_immediate_with_CF W) := {| shrf := shrf |}. - Definition eta_sprl (x : spread_left_immediate W) := {| sprl := sprl |}. - Definition eta_mkl (x : mask_keep_low W) := {| mkl := mkl |}. - Definition eta_and (x : bitwise_and W) := {| and := and |}. - Definition eta_andf (x : bitwise_and_with_CF W) := {| andf := andf |}. - Definition eta_or (x : bitwise_or W) := {| or := or |}. - Definition eta_orf (x : bitwise_or_with_CF W) := {| orf := orf |}. - Definition eta_adc (x : add_with_carry W) := {| adc := adc |}. - Definition eta_subc (x : sub_with_carry W) := {| subc := subc |}. - Definition eta_mul (x : multiply W) := {| mul := mul |}. - Definition eta_mulhwll (x : multiply_low_low W) := {| mulhwll := mulhwll |}. - Definition eta_mulhwhl (x : multiply_high_low W) := {| mulhwhl := mulhwhl |}. - Definition eta_mulhwhh (x : multiply_high_high W) := {| mulhwhh := mulhwhh |}. - Definition eta_muldw (x : multiply_double W) := {| muldw := muldw |}. - Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf := muldwf |}. - Definition eta_selc (x : select_conditional W) := {| selc := selc |}. - Definition eta_addm (x : add_modulo W) := {| addm := addm |}. -End InstructionGallery. - -Declare Reduction unfold_eta_bounded_instructions - := cbv [eta_decode eta_ldi eta_shrd eta_shrdf eta_shl eta_shlf eta_shr eta_shrf eta_sprl eta_mkl eta_and eta_andf eta_or eta_orf eta_adc eta_subc eta_mul eta_mulhwll eta_mulhwhl eta_mulhwhh eta_muldw eta_muldwf eta_selc eta_addm]. - -Module fancy_machine. - Import Interface.fancy_machine. - Definition eta_instructions {n} (x : fancy_machine.instructions n) : fancy_machine.instructions n - := Eval unfold_eta_bounded_instructions in - {| W := W; - decode := eta_decode decode; - ldi := eta_ldi ldi; - shrd := eta_shrd shrd; - shl := eta_shl shl; - shr := eta_shr shr; - adc := eta_adc adc; - subc := eta_subc subc; - mulhwll := eta_mulhwll mulhwll; - mulhwhl := eta_mulhwhl mulhwhl; - mulhwhh := eta_mulhwhh mulhwhh; - selc := eta_selc selc; - addm := eta_addm addm |}. -End fancy_machine. - -Module x86. - Import Interface.x86. - Definition eta_instructions {n} (x : x86.instructions n) : x86.instructions n - := Eval unfold_eta_bounded_instructions in - {| W := W; - decode := eta_decode decode; - ldi := eta_ldi ldi; - shrdf := eta_shrdf shrdf; - shlf := eta_shlf shlf; - shrf := eta_shrf shrf; - adc := eta_adc adc; - subc := eta_subc subc; - muldwf := eta_muldwf muldwf; - selc := eta_selc selc; - orf := eta_orf orf |}. -End x86. diff --git a/src/BoundedArithmetic/StripCF.v b/src/BoundedArithmetic/StripCF.v deleted file mode 100644 index f44b1b7f7..000000000 --- a/src/BoundedArithmetic/StripCF.v +++ /dev/null @@ -1,74 +0,0 @@ -(** * Strip CF for Interface for bounded arithmetic *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.BoundedArithmetic.Interface. - -Local Open Scope type_scope. -Local Open Scope Z_scope. - -Section strip_CF. - Context (n : Z) (* bit-width of width of [W] *) - {W : Type} (* bounded type, [W] for word *) - (Wdecoder : decoder n W). - Local Notation imm := Z (only parsing). (* immediate (compile-time) argument *) - - Global Instance shift_right_doubleword_immediate_strip_CF - {shrdf : shift_right_doubleword_immediate_with_CF W} - : shift_right_doubleword_immediate W - := { shrd x y z := snd (shrdf x y z) }. - Global Instance is_shift_right_doubleword_immediate_strip_CF - {shrdf : shift_right_doubleword_immediate_with_CF W} - {shift_right_doubleword_immediate_with_CF : is_shift_right_doubleword_immediate_with_CF shrdf} - : is_shift_right_doubleword_immediate shift_right_doubleword_immediate_strip_CF - := shift_right_doubleword_immediate_with_CF. - - Global Instance shift_left_immediate_strip_CF - {shlf : shift_left_immediate_with_CF W} - : shift_left_immediate W - := { shl x y := snd (shlf x y) }. - Global Instance is_shift_left_immediate_strip_CF - {shlf : shift_left_immediate_with_CF W} - {shift_left_immediate_with_CF : is_shift_left_immediate_with_CF shlf} - : is_shift_left_immediate shift_left_immediate_strip_CF - := shift_left_immediate_with_CF. - - Global Instance shift_right_immediate_strip_CF - {shrf : shift_right_immediate_with_CF W} - : shift_right_immediate W - := { shr x y := snd (shrf x y) }. - Global Instance is_shift_right_immediate_strip_CF - {shrf : shift_right_immediate_with_CF W} - {shift_right_immediate_with_CF : is_shift_right_immediate_with_CF shrf} - : is_shift_right_immediate shift_right_immediate_strip_CF - := shift_right_immediate_with_CF. - - Global Instance bitwise_and_strip_CF - {andf : bitwise_and_with_CF W} - : bitwise_and W - := { and x y := snd (andf x y) }. - Global Instance is_bitwise_and_strip_CF - {andf : bitwise_and_with_CF W} - {bitwise_and_with_CF : is_bitwise_and_with_CF andf} - : is_bitwise_and bitwise_and_strip_CF - := { decode_bitwise_and := @decode_snd_bitwise_and_with_CF _ _ _ _ bitwise_and_with_CF }. - - Global Instance bitwise_or_strip_CF - {orf : bitwise_or_with_CF W} - : bitwise_or W - := { or x y := snd (orf x y) }. - Global Instance is_bitwise_or_strip_CF - {orf : bitwise_or_with_CF W} - {bitwise_or_with_CF : is_bitwise_or_with_CF orf} - : is_bitwise_or bitwise_or_strip_CF - := { decode_bitwise_or := @decode_snd_bitwise_or_with_CF _ _ _ _ bitwise_or_with_CF }. - - Global Instance multiply_double_strip_CF - {muldwf : multiply_double_with_CF W} - : multiply_double W - := { muldw x y := snd (muldwf x y) }. - Global Instance is_mul_double_strip_CF - {muldwf : multiply_double_with_CF W} - {multiply_double_with_CF : is_mul_double_with_CF muldwf} - : is_mul_double multiply_double_strip_CF - := { decode_fst_mul_double := @decode_fst_mul_double_with_CF _ _ _ _ multiply_double_with_CF; - decode_snd_mul_double := @decode_snd_mul_double_with_CF _ _ _ _ multiply_double_with_CF}. -End strip_CF. diff --git a/src/Experiments/Ed25519_imports.hs b/src/Experiments/Ed25519_imports.hs deleted file mode 100644 index 726b4b268..000000000 --- a/src/Experiments/Ed25519_imports.hs +++ /dev/null @@ -1,5 +0,0 @@ -import qualified Data.List -import qualified Data.Bits -import qualified Data.Word (Word8, Word64) -import qualified Data.ByteString.Lazy as B -import qualified Data.Digest.Pure.SHA as SHA diff --git a/src/Experiments/ExtrHaskellNats.v b/src/Experiments/ExtrHaskellNats.v deleted file mode 100644 index 3e2974ea1..000000000 --- a/src/Experiments/ExtrHaskellNats.v +++ /dev/null @@ -1,111 +0,0 @@ -(** * Extraction Directives for [nat] in Haskell *) -(** [nat] is really complicated, so we jump through many hoops to get - code that compiles in 8.4 and 8.5 at the same time. *) -Require Coq.Numbers.Natural.Peano.NPeano. -Require Coq.Arith.Compare_dec Coq.Arith.EqNat Coq.Arith.Peano_dec. - -Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ] - "(\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))". - - -(** We rely on the fact that Coq forbids masking absolute names. Hopefully we can drop support for 8.4 before this is changed. *) -Module Coq. - Module M. Export NPeano.Nat. End M. - Module Init. - Module Nat. - Export M. - End Nat. - End Init. - Module Numbers. - Module Natural. - Module Peano. - Module NPeano. - Module Nat. - Export M. - End Nat. - End NPeano. - End Peano. - End Natural. - End Numbers. - Module Arith. - Module PeanoNat. - Module Nat. - Export M. - End Nat. - End PeanoNat. - End Arith. -End Coq. - -Module Export Import_NPeano_Nat. - Import Coq.Numbers.Natural.Peano.NPeano.Nat. - - Extract Inlined Constant add => "(Prelude.+)". - Extract Inlined Constant mul => "(Prelude.*)". - Extract Inlined Constant pow => "(Prelude.^)". - Extract Inlined Constant max => "Prelude.max". - Extract Inlined Constant min => "Prelude.min". - Extract Inlined Constant gcd => "Prelude.gcd". - Extract Inlined Constant lcm => "Prelude.lcm". - Extract Inlined Constant land => "(Data.Bits..&.)". - Extract Inlined Constant compare => "Prelude.compare". - Extract Inlined Constant ltb => "(Prelude.<)". - Extract Inlined Constant leb => "(Prelude.<=)". - Extract Inlined Constant eqb => "(Prelude.==)". - Extract Inlined Constant eq_dec => "(Prelude.==)". - Extract Inlined Constant odd => "Prelude.odd". - Extract Inlined Constant even => "Prelude.even". - Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))". - Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". - Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". - Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". - - (* XXX: unsound due to potential overflow in the second argument *) - Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". - Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". - Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". -End Import_NPeano_Nat. - - -Module Export Import_Init_Nat. - Import Coq.Init.Nat. - - Extract Inlined Constant add => "(Prelude.+)". - Extract Inlined Constant mul => "(Prelude.*)". - Extract Inlined Constant max => "Prelude.max". - Extract Inlined Constant min => "Prelude.min". - Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))". - Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". - - Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". - Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". - - (* XXX: unsound due to potential overflow in the second argument *) - Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". - Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". - Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". -End Import_Init_Nat. - - -Module Export Import_PeanoNat_Nat. - Import Coq.Arith.PeanoNat.Nat. - - Extract Inlined Constant eq_dec => "(Prelude.==)". - Extract Inlined Constant add => "(Prelude.+)". - Extract Inlined Constant mul => "(Prelude.*)". - Extract Inlined Constant max => "Prelude.max". - Extract Inlined Constant min => "Prelude.min". - Extract Inlined Constant compare => "Prelude.compare". - - (* XXX: unsound due to potential overflow in the second argument *) - Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". - Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". - Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". -End Import_PeanoNat_Nat. - -Extract Inlined Constant Compare_dec.nat_compare_alt => "Prelude.compare". -Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)". -Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)". -Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)". -Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)". -Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)". -Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)". diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v deleted file mode 100644 index 033ed9363..000000000 --- a/src/Experiments/GenericFieldPow.v +++ /dev/null @@ -1,350 +0,0 @@ -Require Import Coq.setoid_ring.Cring. -Require Import Coq.omega.Omega. -Require Export Crypto.Util.FixCoqMistakes. -Require Import Crypto.Util.Tactics.UniquePose. -(** TODO: Move some imports up here from below, if it doesn't break things *) -Require Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. -Require Coq.setoid_ring.Ring_theory Coq.setoid_ring.NArithRing. -Require Coq.nsatz.Nsatz. -Generalizable All Variables. - - -(*TODO: move *) -Lemma Z_pos_pred_0 p : Z.pos p - 1 = 0 -> p=1%positive. -Proof. destruct p; simpl in *; try discriminate; auto. Qed. - -Lemma Z_neg_succ_neg : forall a b, (Z.neg a + 1)%Z = Z.neg b -> a = Pos.succ b. -Admitted. - -Lemma Z_pos_pred_pos : forall a b, (Z.pos a - 1)%Z = Z.pos b -> a = Pos.succ b. -Admitted. - -Lemma Z_pred_neg p : (Z.neg p - 1)%Z = Z.neg (Pos.succ p). -Admitted. - -(* teach nsatz to deal with the definition of power we are use *) -Instance reify_pow_pos (R:Type) `{Ring R} -e1 lvar t1 n -`{Ring (T:=R)} -{_:reify e1 lvar t1} -: reify (PEpow e1 (N.pos n)) lvar (pow_pos t1 n)|1. - -Class Field_ops (F:Type) - `{Ring_ops F} - {inv:F->F} := {}. - -Class Division (A B C:Type) := division : A -> B -> C. - -Local Notation "_/_" := division. -Local Notation "n / d" := (division n d). - -Module F. - - Definition div `{Field_ops F} n d := n * (inv d). - Global Instance div_notation `{Field_ops F} : @Division F F F := div. - - Class Field {F inv} `{FieldCring:Cring (R:=F)} {Fo:Field_ops F (inv:=inv)} := - { - field_inv_comp : Proper (_==_ ==> _==_) inv; - field_inv_def : forall x, (x == 0 -> False) -> inv x * x == 1; - field_one_neq_zero : not (1 == 0) - }. - Global Existing Instance field_inv_comp. - - Definition powZ `{Field_ops F} (x:F) (n:Z) := - match n with - | Z0 => 1 - | Zpos p => pow_pos x p - | Zneg p => inv (pow_pos x p) - end. - Global Instance power_field `{Field_ops F} : Power | 5 := { power := powZ }. - - Section FieldProofs. - Context `{Field F}. - - Definition unfold_div (x y:F) : x/y = x * inv y := eq_refl. - - Global Instance Proper_div : - Proper (_==_ ==> _==_ ==> _==_) div. - Proof using Type*. - unfold div; repeat intro. - repeat match goal with - | [H: _ == _ |- _ ] => rewrite H; clear H - end; reflexivity. - Qed. - - Global Instance Proper_pow_pos : Proper (_==_==>eq==>_==_) pow_pos. - Proof using Rr. - cut (forall n (y x : F), x == y -> pow_pos x n == pow_pos y n); - [repeat intro; subst; eauto|]. - induction n; simpl; intros; trivial; - repeat eapply ring_mult_comp; eauto. - Qed. - - Global Instance Propper_powZ : Proper (_==_==>eq==>_==_) powZ. - Proof using Type*. - repeat intro; subst; unfold powZ. - match goal with |- context[match ?x with _ => _ end] => destruct x end; - repeat (eapply Proper_pow_pos || f_equiv; trivial). - Qed. - - Import Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. - Lemma field_theory_for_tactic : field_theory 0 1 _+_ _*_ _-_ -_ _/_ inv _==_. - Proof using Type*. - split; repeat constructor; repeat intro; gen_rewrite; try cring; - eauto using field_one_neq_zero, field_inv_def. Qed. - - Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.NArithRing. - Lemma power_theory_for_tactic : power_theory 1 _*_ _==_ NtoZ power. - Proof using Rr. constructor; destruct n; reflexivity. Qed. - - Create HintDb field_nonzero discriminated. - Hint Resolve field_one_neq_zero : field_nonzero. - Ltac field_nonzero := repeat split; auto 3 with field_nonzero. - Ltac field_power_isconst t := Ncst t. - Add Field FieldProofsAddField : field_theory_for_tactic - (postprocess [field_nonzero], - power_tac power_theory_for_tactic [field_power_isconst]). - - Lemma div_mul_idemp_l : forall a b, (a==0 -> False) -> a*b/a == b. - Proof using Type*. intros. field. Qed. - - Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}. - Lemma mul_zero_why : forall a b, a*b == 0 -> a == 0 \/ b == 0. - Proof using Type*. - - intros; destruct (eq_dec a 0); intuition. - assert (a * b / a == 0) by - (match goal with [H: _ == _ |- _ ] => rewrite H; field end). - rewrite div_mul_idemp_l in *; auto. - Qed. - - Import Coq.nsatz.Nsatz. - Global Instance Integral_domain_Field : Integral_domain (R:=F). - Proof using Type*. - constructor; intros; eauto using mul_zero_why, field_one_neq_zero. - Qed. - - Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := - let t := type of H in - generalize H; - field_lookup (PackField FIELD_SIMPL_EQ) [] t; - try (exact I); - try (idtac; []; clear H;intro H). - - Inductive field_simplify_done {x y:F} : (x==y) -> Type := - Field_simplify_done : forall (H:x==y), field_simplify_done H. - Ltac field_nsatz := - repeat match goal with - [ H: _ == _ |- _ ] => - match goal with - | [ Ha : field_simplify_done H |- _ ] => fail - | _ => idtac - end; - field_simplify_eq in H; - unique pose proof (Field_simplify_done H) - end; - repeat match goal with [ H: field_simplify_done _ |- _] => clear H end; - try field_simplify_eq; - try nsatz. - - Create HintDb field discriminated. - Hint Extern 5 (_ == _) => field_nsatz : field. - Hint Extern 5 (_ <-> _) => split. - - Lemma mul_inv_l : forall x, not (x == 0) -> inv x * x == 1. Proof using Type*. auto with field. Qed. - - Lemma mul_inv_r : forall x, not (x == 0) -> x * inv x == 1. Proof using Type*. auto with field. Qed. - - Lemma mul_cancel_r' (x y z:F) : not (z == 0) -> x * z == y * z -> x == y. - Proof using Type*. - intros. - assert (x * z * inv z == y * z * inv z) by - (match goal with [H: _ == _ |- _ ] => rewrite H; auto with field end). - assert (x * z * inv z == x * (z * inv z)) by auto with field. - assert (y * z * inv z == y * (z * inv z)) by auto with field. - rewrite mul_inv_r, @ring_mul_1_r in *; auto with field. - Qed. - - Lemma mul_cancel_r (x y z:F) : not (z == 0) -> (x * z == y * z <-> x == y). - Proof using Type*. intros;split;intros Heq; try eapply mul_cancel_r' in Heq; eauto with field. Qed. - - Lemma mul_cancel_l (x y z:F) : not (z == 0) -> (z * x == z * y <-> x == y). - Proof using Type*. intros;split;intros; try eapply mul_cancel_r; eauto with field. Qed. - - Lemma mul_cancel_r_eq : forall x z:F, not(z==0) -> (x*z == z <-> x == 1). - Proof using Type*. - intros;split;intros Heq; [|nsatz]. - pose proof ring_mul_1_l z as Hz; rewrite <- Hz in Heq at 2; rewrite mul_cancel_r in Heq; eauto. - Qed. - - Lemma mul_cancel_l_eq : forall x z:F, not(z==0) -> (z*x == z <-> x == 1). - Proof using Type*. intros;split;intros Heq; try eapply mul_cancel_r_eq; eauto with field. Qed. - - Lemma inv_unique (a:F) : forall x y, x * a == 1 -> y * a == 1 -> x == y. Proof using Type*. auto with field. Qed. - - Lemma mul_nonzero_nonzero (a b:F) : not (a == 0) -> not (b == 0) -> not (a*b == 0). - Proof using Type*. intros; intro Hab. destruct (mul_zero_why _ _ Hab); auto. Qed. - Hint Resolve mul_nonzero_nonzero : field_nonzero. - - Lemma inv_nonzero (x:F) : not(x == 0) -> not(inv x==0). - Proof using H. - intros Hx Hi. - assert (Hc:not (inv x*x==0)) by (rewrite field_inv_def; eauto with field_nonzero); contradict Hc. - ring [Hi]. - Qed. - Hint Resolve inv_nonzero : field_nonzero. - - Lemma div_nonzero (x y:F) : not(x==0) -> not(y==0) -> not(x/y==0). - Proof using Type*. - unfold division, div_notation, div; auto with field_nonzero. - Qed. - Hint Resolve div_nonzero : field_nonzero. - - Lemma pow_pos_nonzero (x:F) p : not(x==0) -> not(Ncring.pow_pos x p == 0). - Proof using Type*. - intros; induction p using Pos.peano_ind; try assumption; []. - rewrite Ncring.pow_pos_succ; eauto using mul_nonzero_nonzero. - Qed. - Hint Resolve pow_pos_nonzero : field_nonzero. - - Lemma sub_diag_iff (x y:F) : x - y == 0 <-> x == y. Proof using Type*. auto with field. Qed. - - Lemma mul_same (x:F) : x*x == x^2%Z. Proof using Type*. auto with field. Qed. - - Lemma inv_mul (x y:F) : not(x==0) -> not (y==0) -> inv (x*y) == inv x * inv y. - Proof using H. intros;field;intuition. Qed. - - Lemma pow_0_r (x:F) : x^0 == 1. Proof using Type*. auto with field. Qed. - Lemma pow_1_r : forall x:F, x^1%Z == x. Proof using Type*. auto with field. Qed. - Lemma pow_2_r : forall x:F, x^2%Z == x*x. Proof using Type*. auto with field. Qed. - Lemma pow_3_r : forall x:F, x^3%Z == x*x*x. Proof using Type*. auto with field. Qed. - - Lemma pow_succ_r (x:F) (n:Z) : not (x==0)\/(n>=0)%Z -> x^(n+1) == x * x^n. - Proof using Type*. - intros Hnz; unfold power, powZ, power_field, powZ; destruct n eqn:HSn. - - simpl; ring. - - setoid_rewrite <-Pos2Z.inj_succ; rewrite Ncring.pow_pos_succ; ring. - - destruct (Z.succ (Z.neg p)) eqn:Hn. - + assert (p=1%positive) by (destruct p; simpl in *; try discriminate; auto). - subst; simpl in *; field. destruct Hnz; auto with field_nonzero. - + destruct p, p0; discriminate. - + setoid_rewrite Hn. - apply Z_neg_succ_neg in Hn; subst. - rewrite Ncring.pow_pos_succ; field; - destruct Hnz; auto with field_nonzero. - Qed. - - Lemma pow_pred_r (x:F) (n:Z) : not (x==0) -> x^(n-1) == x^n/x. - Proof using Type*. - intros; unfold power, powZ, power_field, powZ; destruct n eqn:HSn. - - simpl. rewrite unfold_div; field. - - destruct (Z.pos p - 1) eqn:Hn. - + apply Z_pos_pred_0 in Hn; subst; simpl; field. - + apply Z_pos_pred_pos in Hn; subst. - rewrite Ncring.pow_pos_succ; field; auto with field_nonzero. - + destruct p; discriminate. - - rewrite Z_pred_neg, Ncring.pow_pos_succ; field; auto with field_nonzero. - Qed. - - Local Ltac pow_peano := - repeat (setoid_rewrite pow_0_r - || setoid_rewrite pow_succ_r - || setoid_rewrite pow_pred_r). - - Lemma pow_mul (x y:F) : forall (n:Z), not(x==0)/\not(y==0)\/(n>=0)%Z -> (x * y)^n == x^n * y^n. - Proof using Type*. - match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end. - { repeat intro. subst. reflexivity. } - - intros; cbv [power power_field powZ]; ring. - - intros n Hn IH Hxy. - repeat setoid_rewrite pow_succ_r; try rewrite IH; try ring; (right; omega). - - intros n Hn IH Hxy. destruct Hxy as [[]|?]; try omega; []. - repeat setoid_rewrite pow_pred_r; try rewrite IH; try field; auto with field_nonzero. - Qed. - - Lemma pow_nonzero (x:F) : forall (n:Z), not(x==0) -> not(x^n==0). - Proof using Type*. - - match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; pow_peano; - eauto with field_nonzero. - { repeat intro. subst. reflexivity. } - Qed. - Hint Resolve pow_nonzero : field_nonzero. - - Lemma pow_inv (x:F) : forall (n:Z), not(x==0) -> inv x^n == inv (x^n). - Proof using Type*. - - match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end. - { repeat intro. subst. reflexivity. } - - intros; cbv [power power_field powZ]. field; eauto with field_nonzero. - - intros n Hn IH Hx. - repeat setoid_rewrite pow_succ_r; try rewrite IH; try field; eauto with field_nonzero. - - intros n Hn IH Hx. - repeat setoid_rewrite pow_pred_r; try rewrite IH; try field; eauto 3 with field_nonzero. - Qed. - - Lemma pow_0_l : forall n, (n>0)%Z -> (0:F)^n==0. - Proof using Type*. - - match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; try omega. - { repeat intro. subst. reflexivity. } - setoid_rewrite pow_succ_r; [auto with field|right;omega]. - Qed. - - Lemma pow_div (x y:F) (n:Z) : not (y==0) -> not(x==0)\/(n >= 0)%Z -> (x/y)^n == x^n/y^n. - Proof using Type*. - intros Hy Hxn. unfold division, div_notation, div. - rewrite pow_mul, pow_inv; try field; destruct Hxn; auto with field_nonzero. - Qed. - - Hint Extern 3 (_ >= _)%Z => omega : field_nonzero. - Lemma issquare_mul (x y z:F) : not (y == 0) -> x^2%Z == z * y^2%Z -> (x/y)^2%Z == z. - Proof using Type*. intros. rewrite pow_div by (auto with field_nonzero); auto with field. Qed. - - Lemma issquare_mul_sub (x y z:F) : 0 == z*y^2%Z - x^2%Z -> (x/y)^2%Z == z \/ x == 0. - Proof using Type*. destruct (eq_dec y 0); [right|left]; auto using issquare_mul with field. Qed. - - Lemma div_mul : forall x y z : F, not(y==0) -> (z == (x / y) <-> z * y == x). - Proof using H. auto with field. Qed. - - Lemma div_1_r : forall x : F, x/1 == x. - Proof using Type*. eauto with field field_nonzero. Qed. - - Lemma div_1_l : forall x : F, not(x==0) -> 1/x == inv x. - Proof using Type*. auto with field. Qed. - - Lemma div_opp_l : forall x y, not (y==0) -> (-_ x) / y == -_ (x / y). - Proof using Type*. auto with field. Qed. - - Lemma div_opp_r : forall x y, not (y==0) -> x / (-_ y) == -_ (x / y). - Proof using Type*. auto with field. Qed. - - Lemma eq_opp_zero : forall x : F, (~ 1 + 1 == (0:F)) -> (x == -_ x <-> x == 0). - Proof using Type*. auto with field. Qed. - - Lemma add_cancel_l : forall x y z:F, z+x == z+y <-> x == y. - Proof using Type*. auto with field. Qed. - - Lemma add_cancel_r : forall x y z:F, x+z == y+z <-> x == y. - Proof using Type*. auto with field. Qed. - - Lemma add_cancel_r_eq : forall x z:F, x+z == z <-> x == 0. - Proof using Type*. auto with field. Qed. - - Lemma add_cancel_l_eq : forall x z:F, z+x == z <-> x == 0. - Proof using Type*. auto with field. Qed. - - Lemma sqrt_solutions : forall x y:F, y ^ 2%Z == x ^ 2%Z -> y == x \/ y == -_ x. - Proof using Type*. - intros ? ? squares_eq. - remember (y - x) as z eqn:Heqz. - assert (y == x + z) as Heqy by (subst; ring); rewrite Heqy in *; clear Heqy Heqz. - assert (Hw:(x + z)^2%Z == z * (x + (x + z)) + x^2%Z) - by (auto with field); rewrite Hw in squares_eq; clear Hw. - rewrite add_cancel_r_eq in squares_eq. - apply mul_zero_why in squares_eq; destruct squares_eq; auto with field. - Qed. - - End FieldProofs. -End F. diff --git a/src/Experiments/c.sh b/src/Experiments/c.sh deleted file mode 100644 index 12757595b..000000000 --- a/src/Experiments/c.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/sh - -cat << EOF -#include <stdint.h> - -typedef struct { uint64_t v[10]; } fe25519; -typedef struct { fe25519 X, Y, Z, T; } ge25519; - -void ge25519_add(ge25519 *R, ge25519 *P, ge25519 *Q) { -EOF - -python -c "print ('\n'.join('\tuint64_t %s_%s_%d = %s->%s.v[%i];'%(P,c,i,P,c,i) for i in range(10) for c in 'XYZT' for P in 'PQ'))" -grep '^\s*(\*\s*let' SpecificCurve25519.v | sed 's#(\*##g' | sed 's#\s*let#\tuint64_t#g' | sed 's#:=#=#g' | sed 's#\s\+in#;#g' | sed 's#\s*\*)##g' -grep -A4 '^\s*(\*\s*let' SpecificCurve25519.v | tail -4 | tr -dc '0123456789x \n' | python -c "import sys; print ('\tge25519 ret = {{' + '},\n\t{'.join(', '.join(line.split()) for line in sys.stdin) + '}};')" - -cat << EOF - *R = ret; -} -EOF diff --git a/src/Specific/SC25519.v b/src/Specific/SC25519.v deleted file mode 100644 index eaf1f564a..000000000 --- a/src/Specific/SC25519.v +++ /dev/null @@ -1,171 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.RelationClasses. -Require Import Crypto.Spec.Ed25519. -Require Import Crypto.EdDSARepChange. -Require Import Crypto.ModularArithmetic.BarrettReduction.ZBounded. -Require Import Crypto.ModularArithmetic.ZBoundedZ. -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.WordUtil. -Import NPeano. - -Local Notation modulusv := (2^252 + 27742317777372353535851937790883648493)%positive. -Local Coercion Z.of_nat : nat >-> Z. -Local Notation eta x := (fst x, snd x). -Local Notation eta3 x := (eta (fst x), snd x). -Local Notation eta4 x := (eta3 (fst x), snd x). -Local Notation eta4' x := (eta (fst x), eta (snd x)). -Local Open Scope Z_scope. - -Section Z. - Definition SRep := Z. (*tuple x86.W (256/n).*) - Definition SRepEq : Relation_Definitions.relation SRep := Logic.eq. - Local Instance SRepEquiv : RelationClasses.Equivalence SRepEq := _. - Local Notation base := 2%Z. - Local Notation kv := 256%Z. - Local Notation offsetv := 8%Z. - Lemma smaller_bound_smaller : (0 <= kv - offsetv <= 256)%Z. Proof. vm_compute; intuition congruence. Qed. - Lemma modulusv_in_range : 0 <= modulusv < 2 ^ 256. Proof. vm_compute; intuition congruence. Qed. - Lemma modulusv_pos : 0 < modulusv. Proof. vm_compute; reflexivity. Qed. - Section params_gen. - Import BarrettBundled. - Local Instance x86_25519_Barrett : BarrettParameters - := { m := modulusv; - b := base; - k := kv; - offset := offsetv; - ops := _; - μ' := base ^ (2 * kv) / modulusv }. - Local Instance x86_25519_BarrettProofs - : BarrettParametersCorrect x86_25519_Barrett - := { props := _ }. - Proof. - vm_compute; reflexivity. - vm_compute; reflexivity. - vm_compute; clear; abstract intuition congruence. - vm_compute; clear; abstract intuition congruence. - vm_compute; clear; abstract intuition congruence. - vm_compute; clear; abstract intuition congruence. - vm_compute; clear; abstract intuition congruence. - vm_compute; reflexivity. - Defined. - End params_gen. - Local Existing Instance x86_25519_Barrett. - Local Existing Instance x86_25519_BarrettProofs. - Declare Reduction srep := cbv [barrett_reduce_function_bundled barrett_reduce_function BarrettBundled.m BarrettBundled.b BarrettBundled.k BarrettBundled.offset BarrettBundled.μ' ZBounded.ConditionalSubtractModulus ZBounded.CarrySubSmall ZBounded.Mod_SmallBound ZBounded.Mod_SmallBound ZBounded.Mul ZBounded.DivBy_SmallBound ZBounded.DivBy_SmallerBound ZBounded.modulus_digits x86_25519_Barrett BarrettBundled.ops ZZLikeOps ZBounded.CarryAdd Z.pow2_mod]. - Definition SRepDecModL : Word.word (256 + 256) -> SRep - := Eval srep in - fun w => dlet w := (Z.of_N (Word.wordToN w)) in barrett_reduce_function_bundled w. - Definition S2Rep : ModularArithmetic.F.F l -> SRep := F.to_Z. - Local Ltac transitivity_refl x := transitivity x; [ | reflexivity ]. - Local Ltac pose_barrett_bounds H x := - pose proof (fun pf => proj1 (barrett_reduce_correct_bundled x pf)) as H; - unfold ZBounded.medium_valid, BarrettBundled.props, x86_25519_BarrettProofs, ZZLikeProperties, BarrettBundled.k in H; - simpl in H. - Local Ltac fold_modulusv := - let m := (eval vm_compute in modulusv) in - change m with modulusv in *. - Local Ltac fold_Z_pow_pos := - repeat match goal with - | [ |- context[Z.pow_pos ?b ?e] ] - => let e2 := (eval compute in (Z.pos e / 2)%Z) in - change (Z.pow_pos b e) with (b^(e2 + e2)) - end; - repeat simpl (Z.pos _ + Z.pos _) in *. - Local Ltac transitivity_barrett_bounds := - let LHS := match goal with |- ?R ?LHS ?RHS => LHS end in - let RHS := match goal with |- ?R ?LHS ?RHS => RHS end in - let H := fresh in - first [ match LHS with - | context[barrett_reduce_function_bundled ?x] - => etransitivity; [ pose_barrett_bounds H x | ] - end - | match RHS with - | context[barrett_reduce_function_bundled ?x] - => symmetry; etransitivity; [ pose_barrett_bounds H x | ] - end ]; - [ apply H; clear H | ]; - instantiate; - rewrite ?Z.pow2_mod_spec in * by omega; - fold_modulusv; fold_Z_pow_pos. - Lemma Z_of_nat_lt_helper x b e : (x < b^e)%nat <-> x < b^e. - Proof. rewrite Nat2Z.inj_lt, Z.pow_Zpow; reflexivity. Qed. - Lemma SRepDecModL_Correct : forall w : Word.word (b + b), SRepEq (S2Rep (ModularArithmetic.F.of_nat l (Word.wordToNat w))) (SRepDecModL w). - Proof. - intro w; unfold SRepEq, S2Rep, b in *. - pose proof (Word.wordToNat_bound w) as H'. - transitivity_refl (barrett_reduce_function_bundled (Z.of_N (Word.wordToN w))). - transitivity_barrett_bounds; - rewrite ?Word.wordToN_nat, ?nat_N_Z, ?WordUtil.pow2_id in *. - { apply Z_of_nat_lt_helper in H'. - rewrite Nat2Z.inj_add in H'. - auto with zarith. } - { reflexivity. } - Qed. - Definition SRepAdd : SRep -> SRep -> SRep - := Eval srep in - let work_around_bug_5198 - := fun x y => barrett_reduce_function_bundled (snd (ZBounded.CarryAdd x y)) - in work_around_bug_5198. - Lemma SRepAdd_Correct : forall x y : ModularArithmetic.F.F l, SRepEq (S2Rep (ModularArithmetic.F.add x y)) (SRepAdd (S2Rep x) (S2Rep y)). - Proof. - intros x y; unfold SRepEq, S2Rep, b in *; simpl. - transitivity_refl (let work_around_bug_5198 - := fun x y => barrett_reduce_function_bundled (snd (ZBounded.CarryAdd x y)) - in work_around_bug_5198 (F.to_Z x) (F.to_Z y)). - pose proof (ModularArithmeticTheorems.F.to_Z_range x). - pose proof (ModularArithmeticTheorems.F.to_Z_range y). - unfold l in *; specialize_by auto using modulusv_pos. - assert (F.to_Z x + F.to_Z y < 2 * modulusv - 1) by omega. - assert (2 * modulusv - 1 <= 2 ^ (kv + kv)) by (vm_compute; clear; intuition congruence). - assert (2 * modulusv - 1 < 2^((kv + offsetv) + (kv + offsetv))) by (vm_compute; clear; intuition congruence). - transitivity_barrett_bounds. - { Z.rewrite_mod_small; omega. } - { rewrite (Z.mod_small _ (base^_)) by zutil_arith. - reflexivity. } - Qed. - Global Instance SRepAdd_Proper : Proper (SRepEq ==> SRepEq ==> SRepEq) SRepAdd. - Proof. unfold SRepEq; repeat intro; subst; reflexivity. Qed. - Definition SRepMul : SRep -> SRep -> SRep - := Eval srep in - let work_around_bug_5198 - := fun x y => barrett_reduce_function_bundled (ZBounded.Mul x y) - in work_around_bug_5198. - Lemma SRepMul_Correct : forall x y : ModularArithmetic.F.F l, SRepEq (S2Rep (ModularArithmetic.F.mul x y)) (SRepMul (S2Rep x) (S2Rep y)). - Proof. - intros x y; unfold SRepEq, S2Rep, b in *; simpl. - transitivity_refl (let work_around_bug_5198 - := fun x y => barrett_reduce_function_bundled (ZBounded.Mul x y) - in work_around_bug_5198 (F.to_Z x) (F.to_Z y)). - pose proof (ModularArithmeticTheorems.F.to_Z_range x). - pose proof (ModularArithmeticTheorems.F.to_Z_range y). - unfold l in *; specialize_by auto using modulusv_pos. - assert (0 <= F.to_Z x * F.to_Z y < modulusv * modulusv) by nia. - assert (modulusv * modulusv <= 2 ^ (kv + kv)) by (vm_compute; clear; intuition congruence). - assert (2^(kv + kv) < 2^((kv + offsetv) + (kv + offsetv))) by (vm_compute; clear; intuition congruence). - transitivity_barrett_bounds. - { Z.rewrite_mod_small; omega. } - { reflexivity. } - Qed. - Global Instance SRepMul_Proper : Proper (SRepEq ==> SRepEq ==> SRepEq) SRepMul. - Proof. unfold SRepEq; repeat intro; subst; reflexivity. Qed. - Definition SRepDecModLShort : Word.word (n + 1) -> SRep - := Eval srep in - fun w => dlet w := (Z.of_N (Word.wordToN w)) in barrett_reduce_function_bundled w. - Lemma SRepDecModLShort_Correct : forall w : Word.word (n + 1), SRepEq (S2Rep (ModularArithmetic.F.of_nat l (Word.wordToNat w))) (SRepDecModLShort w). - Proof. - intros w; unfold SRepEq, S2Rep, n, b in *; simpl. - transitivity_refl (barrett_reduce_function_bundled (Z.of_N (Word.wordToN w))). - transitivity_barrett_bounds. - { pose proof (Word.wordToNat_bound w) as H. - rewrite Word.wordToN_nat, nat_N_Z. - rewrite WordUtil.pow2_id in H. - apply Z_of_nat_lt_helper in H. - rewrite Nat2Z.inj_add in H; simpl @Z.of_nat in *. - split; auto with zarith. - etransitivity; [ eassumption | instantiate; vm_compute; reflexivity ]. } - { rewrite Word.wordToN_nat, nat_N_Z; reflexivity. } - Qed. -End Z. diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4 deleted file mode 100644 index b98067a9a..000000000 --- a/src/SpecificGen/GFtemplate3mod4 +++ /dev/null @@ -1,773 +0,0 @@ -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 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.Tower. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Decidable. -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 precomputation. *) - -Definition modulus : Z := Eval compute in 2^{{{k}}} - {{{c}}}. -Lemma prime_modulus : prime modulus. Admitted. -Definition int_width := Eval compute in (2 * {{{w}}})%Z. -Definition freeze_input_bound := {{{w}}}%Z. - -Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus. - construct_params prime_modulus {{{n}}}%nat {{{k}}}. -Defined. - -Definition length_fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in length limb_widths. -Definition fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in (tuple Z length_fe{{{k}}}{{{c}}}_{{{w}}}). - -Definition mul2modulus : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params{{{k}}}{{{c}}}_{{{w}}})). - -Instance subCoeff : SubtractionCoefficient. - apply Build_SubtractionCoefficient with (coeff := mul2modulus). - vm_decide. -Defined. - -Instance carryChain : CarryChain limb_widths. - apply Build_CarryChain with (carry_chain := (rev {{{ch}}})%nat). - intros. - repeat (destruct H as [|H]; [subst; vm_compute; repeat constructor | ]). - contradiction H. -Defined. - -Definition freezePreconditions : FreezePreconditions freeze_input_bound int_width. -Proof. - constructor; compute_preconditions. -Defined. - -(* Wire format for [pack] and [unpack] *) -Definition wire_widths := Eval compute in (repeat {{{w}}} {{{kdivw}}} ++ {{{kmodw}}} :: nil). - -Definition wire_digits := Eval compute in (tuple Z (length wire_widths)). - -Lemma wire_widths_nonneg : forall w, In w wire_widths -> 0 <= w. -Proof. - intros. - repeat (destruct H as [|H]; [subst; vm_compute; congruence | ]). - contradiction H. -Qed. - -Lemma bits_eq : sum_firstn limb_widths (length limb_widths) = sum_firstn wire_widths (length wire_widths). -Proof. - reflexivity. -Qed. - -Lemma modulus_gt_2 : 2 < modulus. Proof. cbv; congruence. Qed. - -(* Temporarily, we'll use addition chains equivalent to double-and-add. This is pending - finding the real, more optimal chains from previous work. *) -Fixpoint pow2Chain'' p (pow2_index acc_index : nat) chain_acc : list (nat * nat) := - match p with - | xI p' => pow2Chain'' p' 1 0 - (chain_acc ++ (pow2_index, pow2_index) :: (0%nat, S acc_index) :: nil) - | xO p' => pow2Chain'' p' 0 (S acc_index) - (chain_acc ++ (pow2_index, pow2_index)::nil) - | xH => (chain_acc ++ (pow2_index, pow2_index) :: (0%nat, S acc_index) :: nil) - end. - -Fixpoint pow2Chain' p index := - match p with - | xI p' => pow2Chain'' p' 0 0 (repeat (0,0)%nat index) - | xO p' => pow2Chain' p' (S index) - | xH => repeat (0,0)%nat index - end. - -Definition pow2_chain p := - match p with - | xH => nil - | _ => pow2Chain' p 0 - end. - -Definition invChain := Eval compute in pow2_chain (Z.to_pos (modulus - 2)). - -Instance inv_ec : ExponentiationChain (modulus - 2). - apply Build_ExponentiationChain with (chain := invChain). - reflexivity. -Defined. - -(* Note : use caution copying square root code to other primes. The (modulus / 8 + 1) chains are - for primes that are 5 mod 8; if the prime is 3 mod 4 then use (modulus / 4 + 1). *) -Definition sqrtChain := Eval compute in pow2_chain (Z.to_pos (modulus / 4 + 1)). - -Instance sqrt_ec : ExponentiationChain (modulus / 4 + 1). - apply Build_ExponentiationChain with (chain := sqrtChain). - reflexivity. -Defined. - -Arguments chain {_ _ _} _. - -(* END precomputation *) - -(* Precompute constants *) -Definition k_ := Eval compute in k. -Definition k_subst : k = k_ := eq_refl k_. - -Definition c_ := Eval compute in c. -Definition c_subst : c = c_ := eq_refl c_. - -Definition one_ := Eval compute in one. -Definition one_subst : one = one_ := eq_refl one_. - -Definition zero_ := Eval compute in zero. -Definition zero_subst : zero = zero_ := eq_refl zero_. - -Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits. -Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_. - -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemListZOperations.neg ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne. - -Definition app_n2 {T} (f : wire_digits) (P : wire_digits -> T) : T. -Proof. - cbv [wire_digits] in *. - set (f0 := f). - repeat (let g := fresh "g" in destruct f as [f g]). - apply P. - apply f0. -Defined. - -Definition app_n2_correct {T} f (P : wire_digits -> T) : app_n2 f P = P f. -Proof. - intros. - cbv [wire_digits] in *. - repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - reflexivity. -Qed. - -Definition app_n {T} (f : fe{{{k}}}{{{c}}}_{{{w}}}) (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : T. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - set (f0 := f). - repeat (let g := fresh "g" in destruct f as [f g]). - apply P. - apply f0. -Defined. - -Definition app_n_correct {T} f (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : app_n f P = P f. -Proof. - intros. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - reflexivity. -Qed. - -Definition appify2 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (f g : fe{{{k}}}{{{c}}}_{{{w}}}) := - app_n f (fun f0 => (app_n 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_n_correct. -Qed. - -Definition appify9 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe{{{k}}}{{{c}}}_{{{w}}}) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n 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_n_correct | ]); reflexivity. -Qed. - -Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op. -Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op). - -Fixpoint uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} {T} n - : forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n), - Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}}) - := match n - return (forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n), - Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}})) - with - | O => fun x => x - | S n' => fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x => @uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} _ n' (f x)) - end. - -Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 2 op. -Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)). - -Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) - := Eval compute in Tuple.uncurry (n:=length wire_widths) op. -Definition curry_unop_wire_digits {T} op : wire_digits -> T - := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). - -Definition uncurry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 9 op. -Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in - appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 - => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8). - -Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - reflexivity. -Defined. - -Definition add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig add_sig] in - proj1_sig (add_sig f g). - -Definition add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : add f g = add_opt f g := - Eval cbv beta iota delta [proj1_sig add_sig] in - proj2_sig (add_sig f g). - -Definition carry_add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_add_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. - autorewrite with zsimplify_Z_to_pos; cbv. - reflexivity. -Defined. - -Definition carry_add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig carry_add_sig] in - proj1_sig (carry_add_sig f g). - -Definition carry_add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : carry_add f g = carry_add_opt f g := - Eval cbv beta iota delta [proj1_sig carry_add_sig] in - proj2_sig (carry_add_sig f g). - -Definition sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = sub_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - reflexivity. -Defined. - -Definition sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig sub_sig] in - proj1_sig (sub_sig f g). - -Definition sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : sub f g = sub_opt f g := - Eval cbv beta iota delta [proj1_sig sub_sig] in - proj2_sig (sub_sig f g). - -Definition carry_sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_sub_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. - autorewrite with zsimplify_Z_to_pos; cbv. - reflexivity. -Defined. - -Definition carry_sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig carry_sub_sig] in - proj1_sig (carry_sub_sig f g). - -Definition carry_sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : carry_sub f g = carry_sub_opt f g := - Eval cbv beta iota delta [proj1_sig carry_sub_sig] in - proj2_sig (carry_sub_sig f g). - -(* For multiplication, we add another layer of definition so that we can - rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. - It would be much faster if we could take advantage of - the form of [base_from_limb_widths] when doing - division, so we could do subtraction instead. *) - autorewrite with zsimplify_fast. - reflexivity. -Defined. - -Definition mul_simpl (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in - let '{{{enum f}}} := f in - let '{{{enum g}}} := g in - proj1_sig (mul_simpl_sig {{{enum f}}} - {{{enum g}}}). - -Definition mul_simpl_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : mul_simpl f g = carry_mul_opt k_ c_ f g. -Proof. - pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Qed. - -Definition mul_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. -Proof. - eexists. - rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. - autorewrite with zsimplify_Z_to_pos; cbv. - reflexivity. -Defined. - -Definition mul (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig mul_sig] in - proj1_sig (mul_sig f g). - -Definition mul_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : mul f g = carry_mul_opt k_ c_ f g := - Eval cbv beta iota delta [proj1_sig add_sig] in - proj2_sig (mul_sig f g). - -Definition opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = opp_opt f }. -Proof. - eexists. - cbv [opp_opt]. - rewrite <-sub_correct. - rewrite zero_subst. - cbv [sub]. - reflexivity. -Defined. - -Definition opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). - -Definition opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : opp f = opp_opt f - := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). - -Definition carry_opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = carry_opp_opt f }. -Proof. - eexists. - cbv [carry_opp_opt]. - rewrite <-carry_sub_correct. - rewrite zero_subst. - cbv [carry_sub]. - reflexivity. -Defined. - -Definition carry_opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). - -Definition carry_opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : carry_opp f = carry_opp_opt f - := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). - -Definition pow (f : fe{{{k}}}{{{c}}}_{{{w}}}) chain := fold_chain_opt one_ mul chain [f]. - -Lemma pow_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. -Proof. - cbv [pow pow_opt]; intros. - rewrite !fold_chain_opt_correct. - apply Proper_fold_chain; try reflexivity. - intros; subst; apply mul_correct. -Qed. - -(* Now that we have [pow], we can compute sqrt of -1 for use - in sqrt function (this is not needed unless the prime is - 5 mod 8) *) -Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. - -Definition sqrt_m1 := Eval vm_compute in (pow (encode (F.of_Z _ 2)) (pow2_chain (Z.to_pos ((modulus - 1) / 4)))). - -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. - -Definition inv_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = inv_opt k_ c_ one_ f }. -Proof. - eexists; cbv [inv_opt]. - rewrite <-pow_correct. - cbv - [mul]. - reflexivity. -Defined. - -Definition inv (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). - -Definition inv_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : inv f = inv_opt k_ c_ one_ f - := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). - -Definition mbs_field := modular_base_system_field modulus_gt_2. - -Import Morphisms. - -Local Existing Instance prime_modulus. - -Lemma field_and_homomorphisms - : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div - /\ @Ring.is_homomorphism - (F modulus) Logic.eq F.one F.add F.mul - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul encode - /\ @Ring.is_homomorphism - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul - (F modulus) Logic.eq F.one F.add F.mul - decode. -Proof. - eapply @Field.field_and_homomorphism_from_redundant_representation. - { exact (F.field_modulo _). } - { apply encode_rep. } - { reflexivity. } - { reflexivity. } - { reflexivity. } - { intros; rewrite opp_correct, opp_opt_correct; apply opp_rep; reflexivity. } - { intros; rewrite add_correct, add_opt_correct; apply add_rep; reflexivity. } - { intros; rewrite sub_correct, sub_opt_correct; apply sub_rep; reflexivity. } - { intros; rewrite mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. } - { intros; rewrite inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. } - { intros; apply encode_rep. } -Qed. - -Definition field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. - -Lemma carry_field_and_homomorphisms - : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div - /\ @Ring.is_homomorphism - (F modulus) Logic.eq F.one F.add F.mul - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul encode - /\ @Ring.is_homomorphism - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul - (F modulus) Logic.eq F.one F.add F.mul - decode. -Proof. - eapply @Field.field_and_homomorphism_from_redundant_representation. - { exact (F.field_modulo _). } - { apply encode_rep. } - { reflexivity. } - { reflexivity. } - { reflexivity. } - { intros; rewrite carry_opp_correct, carry_opp_opt_correct, carry_opp_rep; apply opp_rep; reflexivity. } - { intros; rewrite carry_add_correct, carry_add_opt_correct, carry_add_rep; apply add_rep; reflexivity. } - { intros; rewrite carry_sub_correct, carry_sub_opt_correct, carry_sub_rep; apply sub_rep; reflexivity. } - { intros; rewrite mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. } - { intros; rewrite inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. } - { intros; apply encode_rep. } -Qed. - -Definition carry_field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. - -Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode. -Proof. apply field_and_homomorphisms. Qed. - -Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_decode - : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. -Proof. apply field_and_homomorphisms. Qed. - - -Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode. -Proof. apply carry_field_and_homomorphisms. Qed. - -Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_decode - : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. -Proof. apply carry_field_and_homomorphisms. Qed. - -Definition ge_modulus_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { b : Z | b = ge_modulus_opt (to_list {{{n}}} f) }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists; cbv [ge_modulus_opt]. - rewrite !modulus_digits_subst. - cbv. - reflexivity. -Defined. - -Definition ge_modulus (f : fe{{{k}}}{{{c}}}_{{{w}}}) : Z := - Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in - let '{{{enum f}}} := f in - proj1_sig (ge_modulus_sig {{{enum f}}}). - -Definition ge_modulus_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - ge_modulus f = ge_modulus_opt (to_list {{{n}}} f). -Proof. - pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Defined. - -Definition prefreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)) }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv - [from_list_default]. - (* TODO(jgross,jadep): use Reflective linearization here? *) - repeat ( - set_evars; rewrite app_Let_In_nd; subst_evars; - eapply Proper_Let_In_nd_changebody; [reflexivity|intro]). - cbv [from_list_default from_list_default']. - reflexivity. -Defined. - -Definition prefreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig prefreeze_sig] in - let '{{{enum f}}} := f in - proj1_sig (prefreeze_sig {{{enum f}}}). - -Definition prefreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : prefreeze f = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)). -Proof. - pose proof (proj2_sig (prefreeze_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Defined. - -Definition postfreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)) }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists; cbv [freeze_opt int_width]. - cbv [to_list to_list']. - cbv [conditional_subtract_modulus_opt]. - rewrite !modulus_digits_subst. - cbv - [from_list_default]. - (* TODO(jgross,jadep): use Reflective linearization here? *) - repeat ( - set_evars; rewrite app_Let_In_nd; subst_evars; - eapply Proper_Let_In_nd_changebody; [reflexivity|intro]). - cbv [from_list_default from_list_default']. - reflexivity. -Defined. - -Definition postfreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig postfreeze_sig] in - let '{{{enum f}}} := f in - proj1_sig (postfreeze_sig {{{enum f}}}). - -Definition postfreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : postfreeze f = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)). -Proof. - pose proof (proj2_sig (postfreeze_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Defined. - -Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - dlet x := prefreeze f in - postfreeze x. - -Local Transparent Let_In. -Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)). -Proof. - cbv [freeze_opt freeze Let_In]. - rewrite prefreeze_correct. - rewrite postfreeze_correct. - match goal with - |- appcontext [to_list _ (from_list_default _ ?n ?xs)] => - assert (length xs = n) as pf; [ | rewrite from_list_default_eq with (pf0 := pf) ] end. - { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. } - rewrite to_list_from_list. - reflexivity. -Qed. -Local Opaque Let_In. - -Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv. - reflexivity. -Defined. - -Definition fieldwiseb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool - := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in - let '{{{enum f}}} := f in - let '{{{enum g}}} := g in - proj1_sig (fieldwiseb_sig {{{enum f}}} - {{{enum g}}}). - -Lemma fieldwiseb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : fieldwiseb f g = @Tuple.fieldwiseb Z Z {{{n}}} Z.eqb f g. -Proof. - set (f' := f); set (g' := g). - hnf in f, g; destruct_head' prod. - exact (proj2_sig (fieldwiseb_sig f' g')). -Qed. - -Definition eqb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { b | b = eqb int_width f g }. -Proof. - cbv [eqb]. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv [ModularBaseSystem.freeze int_width]. - rewrite <-!from_list_default_eq with (d := 0). - rewrite <-!(freeze_opt_correct c_) by auto using length_to_list. - rewrite <-!freeze_correct. - rewrite <-fieldwiseb_correct. - reflexivity. -Defined. - -Definition eqb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool - := Eval cbv beta iota delta [proj1_sig eqb_sig] in - let '{{{enum f}}} := f in - let '{{{enum g}}} := g in - proj1_sig (eqb_sig {{{enum f}}} - {{{enum g}}}). - -Lemma eqb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : eqb f g = ModularBaseSystem.eqb int_width f g. -Proof. - set (f' := f); set (g' := g). - hnf in f, g; destruct_head' prod. - exact (proj2_sig (eqb_sig f' g')). -Qed. - -Definition sqrt_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = sqrt_3mod4_opt k_ c_ one_ f}. -Proof. - eexists. - cbv [sqrt_3mod4_opt int_width]. - rewrite <- pow_correct. - reflexivity. -Defined. - -Definition sqrt (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). - -Definition sqrt_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : sqrt f = sqrt_3mod4_opt k_ c_ one_ f - := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). - -Definition pack_simpl_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv [pack_opt]. - repeat (rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Conversion.convert']). - repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. - cbv [from_list_default_opt]. - reflexivity. -Defined. - -Definition pack_simpl (f : fe{{{k}}}{{{c}}}_{{{w}}}) := - Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in - let '{{{enum f}}} := f in - proj1_sig (pack_simpl_sig {{{enum f}}}). - -Definition pack_simpl_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : pack_simpl f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. -Proof. - pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Qed. - -Definition pack_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - eexists. - rewrite <-pack_simpl_correct. - rewrite <-(@app_n_correct wire_digits). - cbv. - reflexivity. -Defined. - -Definition pack (f : fe{{{k}}}{{{c}}}_{{{w}}}) : wire_digits := - Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). - -Definition pack_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : pack f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). - -Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - cbv [wire_digits] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv [unpack_opt]. - repeat ( - rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Conversion.convert']). - repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. - cbv [from_list_default_opt]. - reflexivity. -Defined. - -Definition unpack_simpl (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in - let '{{{enumw f}}} := f in - proj1_sig (unpack_simpl_sig {{{enumw f}}}). - -Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. -Proof. - pose proof (proj2_sig (unpack_simpl_sig f)). - cbv [wire_digits] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Qed. - -Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - eexists. - rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - reflexivity. -Defined. - -Definition unpack (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). - -Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8 deleted file mode 100644 index d6e8f32ad..000000000 --- a/src/SpecificGen/GFtemplate5mod8 +++ /dev/null @@ -1,782 +0,0 @@ -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 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.Tower. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Decidable. -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 precomputation. *) - -Definition modulus : Z := Eval compute in 2^{{{k}}} - {{{c}}}. -Lemma prime_modulus : prime modulus. Admitted. -Definition int_width := Eval compute in (2 * {{{w}}})%Z. -Definition freeze_input_bound := {{{w}}}%Z. - -Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus. - construct_params prime_modulus {{{n}}}%nat {{{k}}}. -Defined. - -Definition length_fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in length limb_widths. -Definition fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in (tuple Z length_fe{{{k}}}{{{c}}}_{{{w}}}). - -Definition mul2modulus : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params{{{k}}}{{{c}}}_{{{w}}})). - -Instance subCoeff : SubtractionCoefficient. - apply Build_SubtractionCoefficient with (coeff := mul2modulus). - vm_decide. -Defined. - -Instance carryChain : CarryChain limb_widths. - apply Build_CarryChain with (carry_chain := (rev {{{ch}}})%nat). - intros. - repeat (destruct H as [|H]; [subst; vm_compute; repeat constructor | ]). - contradiction H. -Defined. - -Definition freezePreconditions : FreezePreconditions freeze_input_bound int_width. -Proof. - constructor; compute_preconditions. -Defined. - -(* Wire format for [pack] and [unpack] *) -Definition wire_widths := Eval compute in (repeat {{{w}}} {{{kdivw}}} ++ {{{kmodw}}} :: nil). - -Definition wire_digits := Eval compute in (tuple Z (length wire_widths)). - -Lemma wire_widths_nonneg : forall w, In w wire_widths -> 0 <= w. -Proof. - intros. - repeat (destruct H as [|H]; [subst; vm_compute; congruence | ]). - contradiction H. -Qed. - -Lemma bits_eq : sum_firstn limb_widths (length limb_widths) = sum_firstn wire_widths (length wire_widths). -Proof. - reflexivity. -Qed. - -Lemma modulus_gt_2 : 2 < modulus. Proof. cbv; congruence. Qed. - -(* Temporarily, we'll use addition chains equivalent to double-and-add. This is pending - finding the real, more optimal chains from previous work. *) -Fixpoint pow2Chain'' p (pow2_index acc_index : nat) chain_acc : list (nat * nat) := - match p with - | xI p' => pow2Chain'' p' 1 0 - (chain_acc ++ (pow2_index, pow2_index) :: (0%nat, S acc_index) :: nil) - | xO p' => pow2Chain'' p' 0 (S acc_index) - (chain_acc ++ (pow2_index, pow2_index)::nil) - | xH => (chain_acc ++ (pow2_index, pow2_index) :: (0%nat, S acc_index) :: nil) - end. - -Fixpoint pow2Chain' p index := - match p with - | xI p' => pow2Chain'' p' 0 0 (repeat (0,0)%nat index) - | xO p' => pow2Chain' p' (S index) - | xH => repeat (0,0)%nat index - end. - -Definition pow2_chain p := - match p with - | xH => nil - | _ => pow2Chain' p 0 - end. - -Definition invChain := Eval compute in pow2_chain (Z.to_pos (modulus - 2)). - -Instance inv_ec : ExponentiationChain (modulus - 2). - apply Build_ExponentiationChain with (chain := invChain). - reflexivity. -Defined. - -(* Note : use caution copying square root code to other primes. The (modulus / 8 + 1) chains are - for primes that are 5 mod 8; if the prime is 3 mod 4 then use (modulus / 4 + 1). *) -Definition sqrtChain := Eval compute in pow2_chain (Z.to_pos (modulus / 8 + 1)). - -Instance sqrt_ec : ExponentiationChain (modulus / 8 + 1). - apply Build_ExponentiationChain with (chain := sqrtChain). - reflexivity. -Defined. - -Arguments chain {_ _ _} _. - -(* END precomputation *) - -(* Precompute constants *) -Definition k_ := Eval compute in k. -Definition k_subst : k = k_ := eq_refl k_. - -Definition c_ := Eval compute in c. -Definition c_subst : c = c_ := eq_refl c_. - -Definition one_ := Eval compute in one. -Definition one_subst : one = one_ := eq_refl one_. - -Definition zero_ := Eval compute in zero. -Definition zero_subst : zero = zero_ := eq_refl zero_. - -Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits. -Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_. - -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemListZOperations.neg ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne. - -Definition app_n2 {T} (f : wire_digits) (P : wire_digits -> T) : T. -Proof. - cbv [wire_digits] in *. - set (f0 := f). - repeat (let g := fresh "g" in destruct f as [f g]). - apply P. - apply f0. -Defined. - -Definition app_n2_correct {T} f (P : wire_digits -> T) : app_n2 f P = P f. -Proof. - intros. - cbv [wire_digits] in *. - repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - reflexivity. -Qed. - -Definition app_n {T} (f : fe{{{k}}}{{{c}}}_{{{w}}}) (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : T. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - set (f0 := f). - repeat (let g := fresh "g" in destruct f as [f g]). - apply P. - apply f0. -Defined. - -Definition app_n_correct {T} f (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : app_n f P = P f. -Proof. - intros. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - reflexivity. -Qed. - -Definition appify2 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (f g : fe{{{k}}}{{{c}}}_{{{w}}}) := - app_n f (fun f0 => (app_n 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_n_correct. -Qed. - -Definition appify9 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe{{{k}}}{{{c}}}_{{{w}}}) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n 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_n_correct | ]); reflexivity. -Qed. - -Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op. -Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op). - -Fixpoint uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} {T} n - : forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n), - Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}}) - := match n - return (forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n), - Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}})) - with - | O => fun x => x - | S n' => fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x => @uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} _ n' (f x)) - end. - -Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 2 op. -Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)). - -Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) - := Eval compute in Tuple.uncurry (n:=length wire_widths) op. -Definition curry_unop_wire_digits {T} op : wire_digits -> T - := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). - -Definition uncurry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 9 op. -Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in - appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 - => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8). - -Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - reflexivity. -Defined. - -Definition add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig add_sig] in - proj1_sig (add_sig f g). - -Definition add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : add f g = add_opt f g := - Eval cbv beta iota delta [proj1_sig add_sig] in - proj2_sig (add_sig f g). - -Definition carry_add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_add_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. - autorewrite with zsimplify_Z_to_pos; cbv. - reflexivity. -Defined. - -Definition carry_add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig carry_add_sig] in - proj1_sig (carry_add_sig f g). - -Definition carry_add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : carry_add f g = carry_add_opt f g := - Eval cbv beta iota delta [proj1_sig carry_add_sig] in - proj2_sig (carry_add_sig f g). - -Definition sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = sub_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - reflexivity. -Defined. - -Definition sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig sub_sig] in - proj1_sig (sub_sig f g). - -Definition sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : sub f g = sub_opt f g := - Eval cbv beta iota delta [proj1_sig sub_sig] in - proj2_sig (sub_sig f g). - -Definition carry_sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_sub_opt f g}. -Proof. - eexists. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. - autorewrite with zsimplify_Z_to_pos; cbv. - reflexivity. -Defined. - -Definition carry_sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig carry_sub_sig] in - proj1_sig (carry_sub_sig f g). - -Definition carry_sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : carry_sub f g = carry_sub_opt f g := - Eval cbv beta iota delta [proj1_sig carry_sub_sig] in - proj2_sig (carry_sub_sig f g). - -(* For multiplication, we add another layer of definition so that we can - rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. - It would be much faster if we could take advantage of - the form of [base_from_limb_widths] when doing - division, so we could do subtraction instead. *) - autorewrite with zsimplify_fast. - reflexivity. -Defined. - -Definition mul_simpl (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in - let '{{{enum f}}} := f in - let '{{{enum g}}} := g in - proj1_sig (mul_simpl_sig {{{enum f}}} - {{{enum g}}}). - -Definition mul_simpl_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : mul_simpl f g = carry_mul_opt k_ c_ f g. -Proof. - pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Qed. - -Definition mul_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. -Proof. - eexists. - rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. - autorewrite with zsimplify_Z_to_pos; cbv. - reflexivity. -Defined. - -Definition mul (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig mul_sig] in - proj1_sig (mul_sig f g). - -Definition mul_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : mul f g = carry_mul_opt k_ c_ f g := - Eval cbv beta iota delta [proj1_sig add_sig] in - proj2_sig (mul_sig f g). - -Definition opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = opp_opt f }. -Proof. - eexists. - cbv [opp_opt]. - rewrite <-sub_correct. - rewrite zero_subst. - cbv [sub]. - reflexivity. -Defined. - -Definition opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). - -Definition opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : opp f = opp_opt f - := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). - -Definition carry_opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = carry_opp_opt f }. -Proof. - eexists. - cbv [carry_opp_opt]. - rewrite <-carry_sub_correct. - rewrite zero_subst. - cbv [carry_sub]. - reflexivity. -Defined. - -Definition carry_opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). - -Definition carry_opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : carry_opp f = carry_opp_opt f - := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). - -Definition pow (f : fe{{{k}}}{{{c}}}_{{{w}}}) chain := fold_chain_opt one_ mul chain [f]. - -Lemma pow_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. -Proof. - cbv [pow pow_opt]; intros. - rewrite !fold_chain_opt_correct. - apply Proper_fold_chain; try reflexivity. - intros; subst; apply mul_correct. -Qed. - -(* Now that we have [pow], we can compute sqrt of -1 for use - in sqrt function (this is not needed unless the prime is - 5 mod 8) *) -Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. - -Definition sqrt_m1 := Eval vm_compute in (pow (encode (F.of_Z _ 2)) (pow2_chain (Z.to_pos ((modulus - 1) / 4)))). - -Lemma sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F). -Proof. - cbv [rep]. - apply F.eq_to_Z_iff. - vm_compute. - reflexivity. -Qed. - -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. - -Definition inv_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = inv_opt k_ c_ one_ f }. -Proof. - eexists; cbv [inv_opt]. - rewrite <-pow_correct. - cbv - [mul]. - reflexivity. -Defined. - -Definition inv (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). - -Definition inv_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : inv f = inv_opt k_ c_ one_ f - := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). - -Definition mbs_field := modular_base_system_field modulus_gt_2. - -Import Morphisms. - -Local Existing Instance prime_modulus. - -Lemma field_and_homomorphisms - : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div - /\ @Ring.is_homomorphism - (F modulus) Logic.eq F.one F.add F.mul - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul encode - /\ @Ring.is_homomorphism - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul - (F modulus) Logic.eq F.one F.add F.mul - decode. -Proof. - eapply @Field.field_and_homomorphism_from_redundant_representation. - { exact (F.field_modulo _). } - { apply encode_rep. } - { reflexivity. } - { reflexivity. } - { reflexivity. } - { intros; rewrite opp_correct, opp_opt_correct; apply opp_rep; reflexivity. } - { intros; rewrite add_correct, add_opt_correct; apply add_rep; reflexivity. } - { intros; rewrite sub_correct, sub_opt_correct; apply sub_rep; reflexivity. } - { intros; rewrite mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. } - { intros; rewrite inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. } - { intros; apply encode_rep. } -Qed. - -Definition field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. - -Lemma carry_field_and_homomorphisms - : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div - /\ @Ring.is_homomorphism - (F modulus) Logic.eq F.one F.add F.mul - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul encode - /\ @Ring.is_homomorphism - fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul - (F modulus) Logic.eq F.one F.add F.mul - decode. -Proof. - eapply @Field.field_and_homomorphism_from_redundant_representation. - { exact (F.field_modulo _). } - { apply encode_rep. } - { reflexivity. } - { reflexivity. } - { reflexivity. } - { intros; rewrite carry_opp_correct, carry_opp_opt_correct, carry_opp_rep; apply opp_rep; reflexivity. } - { intros; rewrite carry_add_correct, carry_add_opt_correct, carry_add_rep; apply add_rep; reflexivity. } - { intros; rewrite carry_sub_correct, carry_sub_opt_correct, carry_sub_rep; apply sub_rep; reflexivity. } - { intros; rewrite mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. } - { intros; rewrite inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. } - { intros; apply encode_rep. } -Qed. - -Definition carry_field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. - -Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode. -Proof. apply field_and_homomorphisms. Qed. - -Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_decode - : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. -Proof. apply field_and_homomorphisms. Qed. - - -Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode. -Proof. apply carry_field_and_homomorphisms. Qed. - -Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_decode - : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. -Proof. apply carry_field_and_homomorphisms. Qed. - -Definition ge_modulus_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { b : Z | b = ge_modulus_opt (to_list {{{n}}} f) }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists; cbv [ge_modulus_opt]. - rewrite !modulus_digits_subst. - cbv. - reflexivity. -Defined. - -Definition ge_modulus (f : fe{{{k}}}{{{c}}}_{{{w}}}) : Z := - Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in - let '{{{enum f}}} := f in - proj1_sig (ge_modulus_sig {{{enum f}}}). - -Definition ge_modulus_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - ge_modulus f = ge_modulus_opt (to_list {{{n}}} f). -Proof. - pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Defined. - -Definition prefreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)) }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv - [from_list_default]. - (* TODO(jgross,jadep): use Reflective linearization here? *) - repeat ( - set_evars; rewrite app_Let_In_nd; subst_evars; - eapply Proper_Let_In_nd_changebody; [reflexivity|intro]). - cbv [from_list_default from_list_default']. - reflexivity. -Defined. - -Definition prefreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig prefreeze_sig] in - let '{{{enum f}}} := f in - proj1_sig (prefreeze_sig {{{enum f}}}). - -Definition prefreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : prefreeze f = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)). -Proof. - pose proof (proj2_sig (prefreeze_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Defined. - -Definition postfreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)) }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists; cbv [freeze_opt int_width]. - cbv [to_list to_list']. - cbv [conditional_subtract_modulus_opt]. - rewrite !modulus_digits_subst. - cbv - [from_list_default]. - (* TODO(jgross,jadep): use Reflective linearization here? *) - repeat ( - set_evars; rewrite app_Let_In_nd; subst_evars; - eapply Proper_Let_In_nd_changebody; [reflexivity|intro]). - cbv [from_list_default from_list_default']. - reflexivity. -Defined. - -Definition postfreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig postfreeze_sig] in - let '{{{enum f}}} := f in - proj1_sig (postfreeze_sig {{{enum f}}}). - -Definition postfreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : postfreeze f = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)). -Proof. - pose proof (proj2_sig (postfreeze_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Defined. - -Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := - dlet x := prefreeze f in - postfreeze x. - -Local Transparent Let_In. -Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)). -Proof. - cbv [freeze_opt freeze Let_In]. - rewrite prefreeze_correct. - rewrite postfreeze_correct. - match goal with - |- appcontext [to_list _ (from_list_default _ ?n ?xs)] => - assert (length xs = n) as pf; [ | rewrite from_list_default_eq with (pf0 := pf) ] end. - { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. } - rewrite to_list_from_list. - reflexivity. -Qed. -Local Opaque Let_In. - -Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv. - reflexivity. -Defined. - -Definition fieldwiseb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool - := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in - let '{{{enum f}}} := f in - let '{{{enum g}}} := g in - proj1_sig (fieldwiseb_sig {{{enum f}}} - {{{enum g}}}). - -Lemma fieldwiseb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : fieldwiseb f g = @Tuple.fieldwiseb Z Z {{{n}}} Z.eqb f g. -Proof. - set (f' := f); set (g' := g). - hnf in f, g; destruct_head' prod. - exact (proj2_sig (fieldwiseb_sig f' g')). -Qed. - -Definition eqb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : - { b | b = eqb int_width f g }. -Proof. - cbv [eqb]. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv [ModularBaseSystem.freeze int_width]. - rewrite <-!from_list_default_eq with (d := 0). - rewrite <-!(freeze_opt_correct c_) by auto using length_to_list. - rewrite <-!freeze_correct. - rewrite <-fieldwiseb_correct. - reflexivity. -Defined. - -Definition eqb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool - := Eval cbv beta iota delta [proj1_sig eqb_sig] in - let '{{{enum f}}} := f in - let '{{{enum g}}} := g in - proj1_sig (eqb_sig {{{enum f}}} - {{{enum g}}}). - -Lemma eqb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) - : eqb f g = ModularBaseSystem.eqb int_width f g. -Proof. - set (f' := f); set (g' := g). - hnf in f, g; destruct_head' prod. - exact (proj2_sig (eqb_sig f' g')). -Qed. - -Definition sqrt_sig (powx powx_squared f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. -Proof. - eexists. - cbv [sqrt_5mod8_opt int_width]. - apply Proper_Let_In_nd_changebody; [reflexivity|intro]. - set_evars. rewrite <-!mul_correct, <-eqb_correct. subst_evars. - reflexivity. -Defined. - -Definition sqrt (powx powx_squared f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} - := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powx powx_squared f). - -Definition sqrt_correct (powx powx_squared f : fe{{{k}}}{{{c}}}_{{{w}}}) - : sqrt powx powx_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powx powx_squared f - := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powx powx_squared f). - -Definition pack_simpl_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv [pack_opt]. - repeat (rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Conversion.convert']). - repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. - cbv [from_list_default_opt]. - reflexivity. -Defined. - -Definition pack_simpl (f : fe{{{k}}}{{{c}}}_{{{w}}}) := - Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in - let '{{{enum f}}} := f in - proj1_sig (pack_simpl_sig {{{enum f}}}). - -Definition pack_simpl_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : pack_simpl f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. -Proof. - pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Qed. - -Definition pack_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : - { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - eexists. - rewrite <-pack_simpl_correct. - rewrite <-(@app_n_correct wire_digits). - cbv. - reflexivity. -Defined. - -Definition pack (f : fe{{{k}}}{{{c}}}_{{{w}}}) : wire_digits := - Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). - -Definition pack_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) - : pack f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). - -Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - cbv [wire_digits] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists. - cbv [unpack_opt]. - repeat ( - rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Conversion.convert']). - repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. - cbv [from_list_default_opt]. - reflexivity. -Defined. - -Definition unpack_simpl (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in - let '{{{enumw f}}} := f in - proj1_sig (unpack_simpl_sig {{{enumw f}}}). - -Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. -Proof. - pose proof (proj2_sig (unpack_simpl_sig f)). - cbv [wire_digits] in *. - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - assumption. -Qed. - -Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. -Proof. - eexists. - rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe{{{k}}}{{{c}}}_{{{w}}}). - cbv. - reflexivity. -Defined. - -Definition unpack (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := - Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). - -Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/README.md b/src/SpecificGen/README.md deleted file mode 100644 index 165e755d5..000000000 --- a/src/SpecificGen/README.md +++ /dev/null @@ -1,5 +0,0 @@ -Usage: - -python fill_template.py 41417_32.json - -(overwrites GF41417_32.v) diff --git a/src/SpecificGen/copy_bounds.sh b/src/SpecificGen/copy_bounds.sh deleted file mode 100755 index bb43e1aaa..000000000 --- a/src/SpecificGen/copy_bounds.sh +++ /dev/null @@ -1,29 +0,0 @@ -#!/bin/bash - -DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" - -cd "$DIR" - -FILENAME="$1" -V_FILE_STEM="${FILENAME%.*}" -BIT_WIDTH=64 -case "$V_FILE_STEM" in - *_64) BIT_WIDTH=128;; -esac - -if [ -z "$V_FILE_STEM" ]; then - echo "USAGE: $0 JSON_FILE" - exit 1 -fi - -for ORIG in $(git ls-files "../Specific/**GF25519*.v" | grep -v "../Specific/GF25519.v"); do - NEW="$(echo "$ORIG" | sed s'|^../Specific|.|g' | sed s"|25519|${V_FILE_STEM}|g")" - echo "$NEW" - NEW_DIR="$(dirname "$NEW")" - mkdir -p "$NEW_DIR" || exit $? - cat "$ORIG" | sed s"/64/${BIT_WIDTH}/g" | sed s'/Specific/SpecificGen/g' | sed s"/25519/${V_FILE_STEM}/g" > "$NEW" || exit $? - if [ -z "$(git ls-files "$NEW")" ]; then - echo "git add '$NEW'" - git add "$NEW" || exit $? - fi -done diff --git a/src/SpecificGen/fill_template.py b/src/SpecificGen/fill_template.py deleted file mode 100644 index 172ec1079..000000000 --- a/src/SpecificGen/fill_template.py +++ /dev/null @@ -1,39 +0,0 @@ -import os, sys, json - -enum = lambda n, s : "(" + ", ".join([s + str(x) for x in range(n)]) + ")" - -params = open(sys.argv[1]) -replacements = json.load(params) -params.close() -replacements["kmodw"] = replacements["k"] % replacements["w"] -replacements["kdivw"] = int(replacements["k"] / replacements["w"]) -replacements["enum f"] = enum(replacements["n"], "f") -replacements["enum g"] = enum(replacements["n"], "g") -replacements["enumw f"] = enum(replacements["kdivw"] + 1, "f") -replacements = {k : str(v) for k,v in replacements.items()} - -OUT = "GF" + replacements["k"] + replacements["c"] + "_" + replacements["w"] + ".v" - -if len(sys.argv) > 2: - OUT = sys.argv[2] - -if int(replacements["c"]) % 8 == 1: - TEMPLATE = "GFtemplate3mod4" -else: - TEMPLATE = "GFtemplate5mod8" - -BEGIN_FIELD = "{{{" -END_FIELD = "}}}" -field = lambda s : BEGIN_FIELD + s + END_FIELD - -inp = open(TEMPLATE) -out = open(OUT, "w+") - -for line in inp: - new_line = line - for w in replacements: - new_line = new_line.replace(field(w), replacements[w]) - out.write(new_line) - -inp.close() -out.close() |