From 339ee4ec95624751f84997064a6a985478ca5645 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Mar 2019 02:33:39 -0500 Subject: Finish reifying list lemmas After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 22m23.84s | Total | 21m34.63s || +0m49.21s | +3.80% -------------------------------------------------------------------------------------------- 1m52.62s | RewriterRulesInterpGood.vo | 1m37.14s || +0m15.48s | +15.93% 3m25.91s | p384_32.c | 3m14.24s || +0m11.66s | +6.00% 1m32.94s | RewriterRulesGood.vo | 1m42.36s || -0m09.42s | -9.20% 0m33.72s | RewriterWf1.vo | 0m24.30s || +0m09.41s | +38.76% 1m17.31s | Rewriter.vo | 1m12.10s || +0m05.21s | +7.22% 0m43.01s | ExtractionHaskell/unsaturated_solinas | 0m39.84s || +0m03.16s | +7.95% 0m45.21s | p521_32.c | 0m42.86s || +0m02.35s | +5.48% 1m46.30s | Fancy/Barrett256.vo | 1m45.08s || +0m01.21s | +1.16% 0m38.74s | p521_64.c | 0m37.49s || +0m01.25s | +3.33% 0m23.16s | ExtractionOCaml/word_by_word_montgomery | 0m21.44s || +0m01.71s | +8.02% 0m18.74s | p256_32.c | 0m16.88s || +0m01.85s | +11.01% 0m15.00s | ExtractionOCaml/unsaturated_solinas | 0m13.98s || +0m01.01s | +7.29% 0m11.92s | ExtractionOCaml/saturated_solinas | 0m10.13s || +0m01.78s | +17.67% 0m07.82s | ExtractionOCaml/saturated_solinas.ml | 0m05.98s || +0m01.83s | +30.76% 1m47.42s | RewriterWf2.vo | 1m47.81s || -0m00.39s | -0.36% 0m58.35s | ExtractionHaskell/word_by_word_montgomery | 0m57.41s || +0m00.94s | +1.63% 0m45.47s | RewriterInterpProofs1.vo | 0m45.67s || -0m00.20s | -0.43% 0m37.34s | Fancy/Montgomery256.vo | 0m37.09s || +0m00.25s | +0.67% 0m36.14s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.52s || -0m00.38s | -1.04% 0m29.91s | ExtractionHaskell/saturated_solinas | 0m29.70s || +0m00.21s | +0.70% 0m26.77s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.72s || +0m00.05s | +0.18% 0m25.87s | SlowPrimeSynthesisExamples.vo | 0m25.49s || +0m00.38s | +1.49% 0m18.72s | p448_solinas_64.c | 0m19.16s || -0m00.44s | -2.29% 0m16.94s | secp256k1_32.c | 0m17.18s || -0m00.23s | -1.39% 0m13.92s | p434_64.c | 0m13.08s || +0m00.83s | +6.42% 0m13.15s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.58s || +0m00.57s | +4.53% 0m08.97s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.95s || +0m00.02s | +0.22% 0m08.37s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s || -0m00.14s | -1.64% 0m08.35s | p224_32.c | 0m08.10s || +0m00.25s | +3.08% 0m07.77s | p384_64.c | 0m07.29s || +0m00.47s | +6.58% 0m06.92s | BoundsPipeline.vo | 0m06.85s || +0m00.07s | +1.02% 0m05.70s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.14s || -0m00.43s | -7.16% 0m05.12s | ExtractionHaskell/saturated_solinas.hs | 0m06.09s || -0m00.96s | -15.92% 0m03.53s | PushButtonSynthesis/Primitives.vo | 0m03.55s || -0m00.02s | -0.56% 0m03.38s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.04s | +1.19% 0m03.16s | PushButtonSynthesis/BarrettReduction.vo | 0m03.24s || -0m00.08s | -2.46% 0m03.06s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.23s || -0m00.16s | -5.26% 0m02.81s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.84s || -0m00.02s | -1.05% 0m02.62s | curve25519_32.c | 0m02.22s || +0m00.39s | +18.01% 0m01.88s | p224_64.c | 0m01.47s || +0m00.40s | +27.89% 0m01.68s | curve25519_64.c | 0m02.19s || -0m00.51s | -23.28% 0m01.32s | CLI.vo | 0m01.33s || -0m00.01s | -0.75% 0m01.24s | secp256k1_64.c | 0m01.30s || -0m00.06s | -4.61% 0m01.22s | p256_64.c | 0m01.47s || -0m00.25s | -17.00% 0m01.16s | RewriterProofs.vo | 0m01.16s || +0m00.00s | +0.00% 0m01.10s | StandaloneHaskellMain.vo | 0m01.00s || +0m00.10s | +10.00% 0m01.05s | CompilersTestCases.vo | 0m01.09s || -0m00.04s | -3.66% 0m01.04s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.00s | +0.00% --- src/SlowPrimeSynthesisExamples.v | 108 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 108 insertions(+) (limited to 'src/SlowPrimeSynthesisExamples.v') diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index 9bac61295..eb02d9ad6 100644 --- a/src/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -25,6 +25,114 @@ Local Coercion Z.of_nat : nat >-> Z. Local Coercion QArith_base.inject_Z : Z >-> Q. Local Coercion Z.pos : positive >-> Z. +Module debugging_rewriting. + Section __. + Context (n : nat := 2%nat) + (s : Z := 2^127) + (c : list (Z * Z) := [(1,1)]) + (machine_wordsize : Z := 64). + + Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q. + Let idxs := (List.seq 0 n ++ [0; 1])%list%nat. + + Definition possible_values_of_machine_wordsize + := [0; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + + + Let prime_upperbound_list : list Z + := encode_no_reduce (weight (Qnum limbwidth) (Qden limbwidth)) n (s-1). + Let tight_upperbounds : list Z + := List.map + (fun v : Z => Qceiling (11/10 * v)) + prime_upperbound_list. + Definition tight_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds. + Definition loose_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds. + + + Let limbwidth_num := Eval vm_compute in Qnum limbwidth. + Let limbwidth_den := Eval vm_compute in QDen limbwidth. + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f g + => ( (addmod limbwidth_num limbwidth_den n f g) + )) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f g + => ( (add (weight limbwidth_num limbwidth_den) n f g) + )) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f g + => let a_a := to_associational (weight limbwidth_num limbwidth_den) n f in + let b_a := to_associational (weight limbwidth_num limbwidth_den) n g in from_associational (weight limbwidth_num limbwidth_den) n (a_a ++ b_a) + ) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f (g : list Z) + => let a_a := to_associational (weight limbwidth_num limbwidth_den) n f in + a_a) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun (f g : list Z) + => let a_a := combine (map (weight limbwidth_num limbwidth_den) (seq 0 n)) f in + a_a) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Definition foo := (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (combine [1; 2] [1; 2]) in + exact r) + tt + ZRange.type.base.option.None). + + (* + Goal True. + pose foo as X; cbv [foo] in X. + clear -X. + cbv [Pipeline.BoundsPipeline LetIn.Let_In] in X. + set (Y := (PartialEvaluateWithListInfoFromBounds _ _)) in (value of X). + vm_compute in Y. + subst Y; set (Y := (Rewriter.Compilers.PartialEvaluate _)) in (value of X). + cbv [Rewriter.Compilers.PartialEvaluate Rewriter.Compilers.RewriteRules.RewriteNBE Rewriter.Compilers.RewriteRules.Compile.Rewrite Rewriter.Compilers.RewriteRules.Compile.rewrite] in Y. + clear -Y. + change (Rewriter.Compilers.RewriteRules.nbe_default_fuel) with (S (pred Rewriter.Compilers.RewriteRules.nbe_default_fuel)) in (value of Y). + cbn [Rewriter.Compilers.RewriteRules.Compile.repeat_rewrite] in Y. + cbv [Rewriter.Compilers.RewriteRules.Compile.rewrite_bottomup] in Y. + Print Rewriter.Compilers.RewriteRules.nbe_rewrite_head. + Abort. + *) + End __. +End debugging_rewriting. + Section debugging_p448. Context (n : nat := 8%nat) (s : Z := 2^448) -- cgit v1.2.3