aboutsummaryrefslogtreecommitdiff
path: root/src/Rewriter.v
Commit message (Collapse)AuthorAge
* Clean up notations after bbv removalHEADmasterGravatar Benjamin Barenblat2019-04-26
| | | | | | | Restore `Reserved Notation` directives for `$ x` and `# x`, which were commented out to avoid conflicts with bbv. Make both notations `at level 9, x at level 9`, which matches unary prefix operators throughout the rest of the development.
* Do less reduction in GENERATEDIdentifiersWithoutTypesGravatar Jason Gross2019-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since more of the definitions are now done in Gallina, hopefully these should be easier to factor out / parameterize over the type of identifiers, now. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 21m28.78s | Total | 21m49.80s || -0m21.01s | -1.60% ----------------------------------------------------------------------------------------------- 0m22.98s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m49.53s || -0m26.55s | -53.60% 0m47.26s | p521_32.c | 0m44.08s || +0m03.17s | +7.21% 0m36.30s | ExtractionHaskell/saturated_solinas | 0m32.96s || +0m03.33s | +10.13% 1m00.34s | ExtractionHaskell/word_by_word_montgomery | 1m02.45s || -0m02.10s | -3.37% 0m26.90s | SlowPrimeSynthesisExamples.vo | 0m24.35s || +0m02.54s | +10.47% 0m16.06s | GENERATEDIdentifiersWithoutTypes.vo | 0m19.05s || -0m02.99s | -15.69% 0m14.89s | ExtractionOCaml/unsaturated_solinas | 0m12.83s || +0m02.06s | +16.05% 0m43.92s | ExtractionHaskell/unsaturated_solinas | 0m42.40s || +0m01.52s | +3.58% 0m20.11s | ExtractionOCaml/word_by_word_montgomery | 0m21.19s || -0m01.08s | -5.09% 0m20.06s | p256_32.c | 0m21.81s || -0m01.75s | -8.02% 0m17.96s | secp256k1_32.c | 0m19.45s || -0m01.48s | -7.66% 0m13.58s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.89s || -0m01.31s | -8.79% 0m07.27s | ExtractionOCaml/saturated_solinas.ml | 0m05.75s || +0m01.51s | +26.43% 3m23.62s | p384_32.c | 3m23.29s || +0m00.33s | +0.16% 1m42.18s | Fancy/Barrett256.vo | 1m41.69s || +0m00.49s | +0.48% 1m33.94s | RewriterWf2.vo | 1m34.43s || -0m00.49s | -0.51% 0m55.14s | Rewriter/ToFancyWithCasts.vo | 0m55.92s || -0m00.78s | -1.39% 0m46.15s | Rewriter/NBE.vo | 0m46.06s || +0m00.08s | +0.19% 0m44.70s | Rewriter/ArithWithCasts.vo | 0m44.55s || +0m00.15s | +0.33% 0m43.96s | RewriterInterpProofs1.vo | 0m44.18s || -0m00.21s | -0.49% 0m39.78s | p521_64.c | 0m38.84s || +0m00.93s | +2.42% 0m36.72s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.54s || +0m00.17s | +0.49% 0m35.92s | RewriterWf1.vo | 0m36.26s || -0m00.33s | -0.93% 0m34.57s | Fancy/Montgomery256.vo | 0m34.64s || -0m00.07s | -0.20% 0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.17s || +0m00.11s | +0.44% 0m23.67s | Rewriter/Arith.vo | 0m24.59s || -0m00.91s | -3.74% 0m20.78s | PushButtonSynthesis/BarrettReduction.vo | 0m20.69s || +0m00.08s | +0.43% 0m18.97s | p448_solinas_64.c | 0m18.10s || +0m00.86s | +4.80% 0m14.02s | p434_64.c | 0m13.37s || +0m00.65s | +4.86% 0m11.26s | ExtractionOCaml/unsaturated_solinas.ml | 0m10.61s || +0m00.65s | +6.12% 0m10.76s | ExtractionOCaml/saturated_solinas | 0m11.65s || -0m00.89s | -7.63% 0m08.76s | p224_32.c | 0m09.58s || -0m00.82s | -8.55% 0m08.07s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.96s || +0m00.11s | +1.38% 0m07.88s | p384_64.c | 0m08.81s || -0m00.93s | -10.55% 0m06.98s | BoundsPipeline.vo | 0m06.97s || +0m00.01s | +0.14% 0m06.41s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.52s || +0m00.89s | +16.12% 0m05.21s | ExtractionHaskell/saturated_solinas.hs | 0m04.48s || +0m00.72s | +16.29% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.61s || -0m00.06s | -1.93% 0m03.33s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.04s | -1.47% 0m03.20s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.02s | -0.62% 0m03.05s | curve25519_32.c | 0m02.76s || +0m00.29s | +10.50% 0m02.63s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.70s || -0m00.07s | -2.59% 0m02.53s | Rewriter.vo | 0m02.04s || +0m00.48s | +24.01% 0m02.10s | curve25519_64.c | 0m01.80s || +0m00.30s | +16.66% 0m01.94s | p224_64.c | 0m01.52s || +0m00.41s | +27.63% 0m01.85s | secp256k1_64.c | 0m01.55s || +0m00.30s | +19.35% 0m01.40s | CLI.vo | 0m01.33s || +0m00.06s | +5.26% 0m01.36s | p256_64.c | 0m01.84s || -0m00.48s | -26.08% 0m01.33s | Rewriter/StripLiteralCasts.vo | 0m01.22s || +0m00.11s | +9.01% 0m01.23s | CompilersTestCases.vo | 0m01.14s || +0m00.09s | +7.89% 0m01.15s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.03s | +3.60% 0m01.13s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.04s | -3.41% 0m01.11s | Rewriter/ToFancy.vo | 0m01.07s || +0m00.04s | +3.73% 0m00.80s | RewriterAll.vo | 0m00.80s || +0m00.00s | +0.00% 0m00.74s | RewriterAllTactics.vo | 0m00.91s || -0m00.17s | -18.68% The diff in the .ml files is quite small, and is effectively just variable renaming: ```diff diff --git a/src/ExtractionOCaml/saturated_solinas.ml b/src/ExtractionOCaml/saturated_solinas.ml index fd8a9d3..e9afa49 100644 --- a/src/ExtractionOCaml/saturated_solinas.ml +++ b/src/ExtractionOCaml/saturated_solinas.ml @@ -39856,7 +39856,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -39962,7 +39962,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40068,7 +40068,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40174,7 +40174,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40280,7 +40280,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49466,8 +49466,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/unsaturated_solinas.ml b/src/ExtractionOCaml/unsaturated_solinas.ml index 473992c..4d4d604 100644 --- a/src/ExtractionOCaml/unsaturated_solinas.ml +++ b/src/ExtractionOCaml/unsaturated_solinas.ml @@ -40045,7 +40045,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40151,7 +40151,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40257,7 +40257,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40363,7 +40363,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40469,7 +40469,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49655,8 +49655,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/word_by_word_montgomery.ml b/src/ExtractionOCaml/word_by_word_montgomery.ml index f955bc6..a672b5d 100644 --- a/src/ExtractionOCaml/word_by_word_montgomery.ml +++ b/src/ExtractionOCaml/word_by_word_montgomery.ml @@ -39944,7 +39944,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40050,7 +40050,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40156,7 +40156,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40262,7 +40262,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40368,7 +40368,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49554,8 +49554,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None ```
* Replace the python script with Ltac codeGravatar Jason Gross2019-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now rely on Ltac rather than python to generate the raw identifiers. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 22m05.90s | Total | 21m51.87s || +0m14.03s | +1.07% ----------------------------------------------------------------------------------------------- 0m49.25s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m55.23s || -0m05.97s | -10.82% 0m19.14s | GENERATEDIdentifiersWithoutTypes.vo | 0m13.35s || +0m05.79s | +43.37% 0m36.52s | ExtractionHaskell/saturated_solinas | 0m32.60s || +0m03.92s | +12.02% 0m24.00s | SlowPrimeSynthesisExamples.vo | 0m27.22s || -0m03.21s | -11.82% 0m08.55s | ExtractionOCaml/saturated_solinas.ml | 0m05.49s || +0m03.06s | +55.73% 3m24.98s | p384_32.c | 3m22.52s || +0m02.45s | +1.21% 1m03.78s | ExtractionHaskell/word_by_word_montgomery | 1m01.13s || +0m02.64s | +4.33% 0m47.85s | p521_32.c | 0m45.77s || +0m02.07s | +4.54% 1m42.64s | Fancy/Barrett256.vo | 1m41.49s || +0m01.14s | +1.13% 0m40.30s | p521_64.c | 0m42.20s || -0m01.90s | -4.50% 0m18.02s | p256_32.c | 0m19.03s || -0m01.01s | -5.30% 0m14.70s | ExtractionOCaml/unsaturated_solinas | 0m13.33s || +0m01.36s | +10.27% 0m14.28s | p434_64.c | 0m15.39s || -0m01.11s | -7.21% 0m09.82s | p224_32.c | 0m08.77s || +0m01.05s | +11.97% 0m08.59s | p384_64.c | 0m07.36s || +0m01.22s | +16.71% 0m05.18s | ExtractionHaskell/saturated_solinas.hs | 0m06.59s || -0m01.41s | -21.39% 1m34.02s | RewriterWf2.vo | 1m34.23s || -0m00.20s | -0.22% 0m56.16s | Rewriter/ToFancyWithCasts.vo | 0m55.41s || +0m00.75s | +1.35% 0m45.85s | Rewriter/NBE.vo | 0m45.23s || +0m00.62s | +1.37% 0m44.51s | Rewriter/ArithWithCasts.vo | 0m44.12s || +0m00.39s | +0.88% 0m44.10s | RewriterInterpProofs1.vo | 0m43.89s || +0m00.21s | +0.47% 0m43.66s | ExtractionHaskell/unsaturated_solinas | 0m43.25s || +0m00.40s | +0.94% 0m36.46s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.36s || +0m00.10s | +0.27% 0m36.09s | RewriterWf1.vo | 0m36.07s || +0m00.02s | +0.05% 0m34.50s | Fancy/Montgomery256.vo | 0m34.30s || +0m00.20s | +0.58% 0m27.13s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.99s || +0m00.14s | +0.51% 0m24.70s | Rewriter/Arith.vo | 0m24.26s || +0m00.43s | +1.81% 0m22.75s | ExtractionOCaml/word_by_word_montgomery | 0m22.15s || +0m00.60s | +2.70% 0m20.96s | PushButtonSynthesis/BarrettReduction.vo | 0m20.74s || +0m00.22s | +1.06% 0m18.96s | p448_solinas_64.c | 0m19.32s || -0m00.35s | -1.86% 0m18.16s | secp256k1_32.c | 0m18.13s || +0m00.03s | +0.16% 0m14.62s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.77s || +0m00.84s | +6.17% 0m11.84s | ExtractionOCaml/saturated_solinas | 0m11.30s || +0m00.53s | +4.77% 0m09.55s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.14s || +0m00.41s | +4.48% 0m08.42s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.16s || +0m00.25s | +3.18% 0m06.96s | BoundsPipeline.vo | 0m06.85s || +0m00.11s | +1.60% 0m06.54s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.17s || -0m00.62s | -8.78% 0m03.57s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.10s | +3.17% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.01s | +0.29% 0m03.30s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || +0m00.07s | +2.48% 0m02.83s | curve25519_32.c | 0m02.86s || -0m00.02s | -1.04% 0m02.70s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.63s || +0m00.07s | +2.66% 0m02.08s | Rewriter.vo | 0m02.02s || +0m00.06s | +2.97% 0m01.60s | curve25519_64.c | 0m01.82s || -0m00.21s | -12.08% 0m01.47s | secp256k1_64.c | 0m01.94s || -0m00.47s | -24.22% 0m01.34s | p224_64.c | 0m01.71s || -0m00.36s | -21.63% 0m01.33s | CLI.vo | 0m01.38s || -0m00.04s | -3.62% 0m01.32s | p256_64.c | 0m01.77s || -0m00.44s | -25.42% 0m01.28s | Rewriter/ToFancy.vo | 0m01.36s || -0m00.08s | -5.88% 0m01.23s | Rewriter/StripLiteralCasts.vo | 0m01.08s || +0m00.14s | +13.88% 0m01.16s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.02s | -1.69% 0m01.13s | CompilersTestCases.vo | 0m01.18s || -0m00.05s | -4.23% 0m01.07s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.05s | -4.46% 0m00.83s | RewriterAll.vo | 0m00.66s || +0m00.16s | +25.75% 0m00.78s | RewriterAllTactics.vo | 0m00.83s || -0m00.04s | -6.02%
* Automate more of the rewriter, and factor out rule-specific thingsGravatar Jason Gross2019-04-11
|
* Automate more of the rewriter reification, proofGravatar Jason Gross2019-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now we actually make use of the rewrite-rule-specific proofs, rather than duplicating them inline. We now support reifying `ident.gets_inlined` to `SubstVarLike.is_var_fst_snd_pair_opp_cast`. We also now fix a bug where we previously incorrectly substituted context variables when reifying side conditions (needed for correct reification of split-mul things, coming up soon). Things are unfortunately a bit slow. I'm not sure what's up with my proof of `reflect_ident_iota_interp_related`; it seems more complicated than it should be (maybe partly due to funext concerns). Next up is to split out the rewrite rule generation bits into separate files and have a single tactic that builds the entire package for us (in prep for making the rewriter builder a vernacular). After that I want to more fully parameterize things over `ident`, and then also over the non-container base-types (which will require some reworking of how we handle special identifiers). Additionally, I want to make the rewrite rule definitions not depend on Language.v. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m50.18s | Total | 23m01.24s || -2m11.06s | -9.48% ----------------------------------------------------------------------------------------------- 0m27.24s | RewriterRulesGood.vo | 1m34.94s || -1m07.70s | -71.30% 0m54.89s | RewriterRulesInterpGood.vo | 1m57.72s || -1m02.82s | -53.37% 1m37.88s | RewriterWf2.vo | 1m47.69s || -0m09.81s | -9.10% 1m16.71s | Rewriter.vo | 1m12.61s || +0m04.10s | +5.64% 0m37.14s | ExtractionHaskell/unsaturated_solinas | 0m40.06s || -0m02.92s | -7.28% 0m36.10s | RewriterWf1.vo | 0m33.12s || +0m02.98s | +8.99% 0m18.31s | p256_32.c | 0m20.70s || -0m02.39s | -11.54% 1m43.31s | Fancy/Barrett256.vo | 1m42.09s || +0m01.21s | +1.19% 0m32.46s | ExtractionHaskell/saturated_solinas | 0m30.92s || +0m01.53s | +4.98% 0m23.44s | ExtractionOCaml/word_by_word_montgomery | 0m22.26s || +0m01.17s | +5.30% 0m12.17s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.58s || -0m01.41s | -10.38% 0m10.04s | p224_32.c | 0m08.20s || +0m01.83s | +22.43% 0m09.98s | ExtractionOCaml/saturated_solinas | 0m11.67s || -0m01.68s | -14.48% 0m07.80s | ExtractionOCaml/saturated_solinas.ml | 0m06.16s || +0m01.63s | +26.62% 0m06.87s | ExtractionHaskell/saturated_solinas.hs | 0m04.98s || +0m01.88s | +37.95% 3m23.11s | p384_32.c | 3m22.61s || +0m00.50s | +0.24% 0m59.32s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || +0m00.56s | +0.95% 0m46.19s | p521_32.c | 0m47.16s || -0m00.96s | -2.05% 0m45.26s | RewriterInterpProofs1.vo | 0m45.64s || -0m00.38s | -0.83% 0m39.50s | p521_64.c | 0m38.97s || +0m00.53s | +1.36% 0m36.38s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.00s || +0m00.38s | +1.05% 0m34.40s | Fancy/Montgomery256.vo | 0m34.63s || -0m00.23s | -0.66% 0m26.95s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.44s || +0m00.50s | +1.92% 0m25.62s | SlowPrimeSynthesisExamples.vo | 0m26.04s || -0m00.41s | -1.61% 0m24.39s | RewriterRulesProofs.vo | 0m24.18s || +0m00.21s | +0.86% 0m20.49s | PushButtonSynthesis/BarrettReduction.vo | 0m20.62s || -0m00.13s | -0.63% 0m18.54s | p448_solinas_64.c | 0m19.15s || -0m00.60s | -3.18% 0m17.37s | secp256k1_32.c | 0m17.70s || -0m00.32s | -1.86% 0m14.80s | p434_64.c | 0m14.16s || +0m00.64s | +4.51% 0m14.05s | ExtractionOCaml/unsaturated_solinas | 0m14.28s || -0m00.22s | -1.61% 0m09.17s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.58s || -0m00.41s | -4.27% 0m08.47s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.22s || +0m00.25s | +3.04% 0m07.69s | p384_64.c | 0m07.72s || -0m00.02s | -0.38% 0m06.80s | BoundsPipeline.vo | 0m06.65s || +0m00.14s | +2.25% 0m06.49s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.59s || +0m00.90s | +16.10% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.08s | +2.31% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.36s || -0m00.00s | -0.29% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.15s || +0m00.04s | +1.26% 0m02.79s | curve25519_32.c | 0m03.32s || -0m00.52s | -15.96% 0m02.66s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s || -0m00.06s | -2.56% 0m02.55s | RewriterRules.vo | 0m02.52s || +0m00.02s | +1.19% 0m01.98s | curve25519_64.c | 0m01.57s || +0m00.40s | +26.11% 0m01.78s | p224_64.c | 0m01.30s || +0m00.48s | +36.92% 0m01.60s | secp256k1_64.c | 0m01.74s || -0m00.13s | -8.04% 0m01.45s | p256_64.c | 0m01.55s || -0m00.10s | -6.45% 0m01.34s | RewriterProofs.vo | 0m01.16s || +0m00.18s | +15.51% 0m01.33s | CLI.vo | 0m01.40s || -0m00.06s | -4.99% 0m01.12s | StandaloneOCamlMain.vo | 0m01.09s || +0m00.03s | +2.75% 0m01.10s | CompilersTestCases.vo | 0m01.08s || +0m00.02s | +1.85% 0m01.08s | StandaloneHaskellMain.vo | 0m01.02s || +0m00.06s | +5.88%
* Add UnderLets flat_map interp proofs,other changesGravatar Jason Gross2019-04-04
| | | | | | | | Also remove a rewrite rule using cast from the non-cast arith rules, regenerate the .out files, add ident.gets_inlined for eventual use in the rewriter, and generalize the rewrite rule lemmas over cast_out_of_range so that we can actually make use of their proofs for interp.
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
|
* Factor out rewriter rulesGravatar Jason Gross2019-03-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move rewrite rule definitions, and the proofs about them, into separate files. We don't yet make use of the separate interp proofs of rewrite rules; the next step is to refactor the interp proof machinery so that we can easily prove the relevant interp relations, given the equality proofs in `src/RewriterRulesProofs.v` After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 23m01.93s | Total | 22m37.08s || +0m24.84s | +1.83% -------------------------------------------------------------------------------------------- 0m24.10s | RewriterRulesProofs.vo | N/A || +0m24.10s | ∞ 1m12.13s | Rewriter.vo | 1m20.61s || -0m08.48s | -10.51% 0m41.17s | ExtractionHaskell/unsaturated_solinas | 0m37.57s || +0m03.60s | +9.58% 1m42.40s | Fancy/Barrett256.vo | 1m40.22s || +0m02.18s | +2.17% 0m45.56s | p521_32.c | 0m48.16s || -0m02.59s | -5.39% 0m14.48s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.47s || +0m02.00s | +16.11% 1m48.48s | RewriterWf2.vo | 1m46.70s || +0m01.77s | +1.66% 0m15.06s | ExtractionOCaml/unsaturated_solinas | 0m14.06s || +0m01.00s | +7.11% 0m06.26s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.29s || -0m01.03s | -14.12% 0m04.71s | ExtractionHaskell/saturated_solinas.hs | 0m06.05s || -0m01.33s | -22.14% 3m22.17s | p384_32.c | 3m23.06s || -0m00.88s | -0.43% 1m57.31s | RewriterRulesInterpGood.vo | 1m56.61s || +0m00.70s | +0.60% 1m35.20s | RewriterRulesGood.vo | 1m35.80s || -0m00.59s | -0.62% 0m57.50s | ExtractionHaskell/word_by_word_montgomery | 0m56.53s || +0m00.96s | +1.71% 0m45.71s | RewriterInterpProofs1.vo | 0m46.13s || -0m00.42s | -0.91% 0m39.66s | p521_64.c | 0m38.90s || +0m00.75s | +1.95% 0m36.22s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.42s || -0m00.20s | -0.54% 0m34.39s | Fancy/Montgomery256.vo | 0m34.45s || -0m00.06s | -0.17% 0m33.16s | RewriterWf1.vo | 0m32.96s || +0m00.19s | +0.60% 0m32.21s | ExtractionHaskell/saturated_solinas | 0m31.53s || +0m00.67s | +2.15% 0m26.94s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.20s || -0m00.25s | -0.95% 0m25.89s | SlowPrimeSynthesisExamples.vo | 0m25.59s || +0m00.30s | +1.17% 0m23.37s | ExtractionOCaml/word_by_word_montgomery | 0m22.90s || +0m00.47s | +2.05% 0m21.19s | PushButtonSynthesis/BarrettReduction.vo | 0m20.79s || +0m00.40s | +1.92% 0m18.30s | p256_32.c | 0m18.54s || -0m00.23s | -1.29% 0m18.29s | p448_solinas_64.c | 0m18.58s || -0m00.28s | -1.56% 0m17.92s | secp256k1_32.c | 0m18.41s || -0m00.48s | -2.66% 0m14.06s | p434_64.c | 0m13.92s || +0m00.14s | +1.00% 0m11.61s | ExtractionOCaml/saturated_solinas | 0m11.57s || +0m00.03s | +0.34% 0m08.90s | p224_32.c | 0m09.12s || -0m00.21s | -2.41% 0m08.49s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.85s || -0m00.35s | -4.06% 0m08.45s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.62s || -0m00.16s | -1.97% 0m08.02s | p384_64.c | 0m07.04s || +0m00.97s | +13.92% 0m07.01s | ExtractionOCaml/saturated_solinas.ml | 0m06.57s || +0m00.43s | +6.69% 0m06.67s | BoundsPipeline.vo | 0m06.87s || -0m00.20s | -2.91% 0m03.39s | PushButtonSynthesis/Primitives.vo | 0m03.44s || -0m00.04s | -1.45% 0m03.36s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.02s | -0.59% 0m03.23s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.21s || +0m00.02s | +0.62% 0m03.04s | curve25519_32.c | 0m02.68s || +0m00.35s | +13.43% 0m02.74s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.55s || +0m00.19s | +7.45% 0m02.19s | curve25519_64.c | 0m01.81s || +0m00.37s | +20.99% 0m01.72s | secp256k1_64.c | 0m01.46s || +0m00.26s | +17.80% 0m01.56s | p256_64.c | 0m01.22s || +0m00.34s | +27.86% 0m01.49s | p224_64.c | 0m01.56s || -0m00.07s | -4.48% 0m01.32s | CLI.vo | 0m01.32s || +0m00.00s | +0.00% 0m01.14s | StandaloneHaskellMain.vo | 0m01.08s || +0m00.05s | +5.55% 0m01.06s | CompilersTestCases.vo | 0m01.04s || +0m00.02s | +1.92% 0m01.06s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.06s | -5.35% 0m01.00s | RewriterProofs.vo | 0m01.13s || -0m00.12s | -11.50% 0m00.64s | RewriterRules.vo | N/A || +0m00.64s | ∞
* Fix a non-terminated commentGravatar Jason Gross2019-03-31
|
* Add some comments based on CR requestsGravatar Jason Gross2019-03-31
|
* Finish reifying list lemmasGravatar Jason Gross2019-03-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
| | | | | | | | | | | | | Rather than taking the convention that failures during constr construction emit a type error from `I : I` with the actual error message `idtac`d above them (because Coq has no way to emit multiple things on stderr), we instead factor everything through a new `constr_fail` or `constr_fail_with msg_tac`, which emit more helpful messages instructing the user to look in `*coq*` or to use `Fail`/`try` to see the more informative error message. When we can make our own version that does both `idtac` and `fail` (c.f. https://github.com/coq/coq/issues/3913), then we can do something a bit more sane, hopefully.
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
|
* Reify most rewrite rulesGravatar Jason Gross2019-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently we don't handle rules that require "concrete list of cons cells" nor rules that require "concrete nat literal to do recursion on"; both of these require special treatment, to be implemented in an upcoming commit. The reifier is kind-of slow, alas. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m52.72s | Total | 21m20.90s || +0m31.82s | +2.48% -------------------------------------------------------------------------------------------- 1m12.22s | Rewriter.vo | 0m47.38s || +0m24.83s | +52.42% 3m14.35s | p384_32.c | 3m19.59s || -0m05.24s | -2.62% 1m45.12s | RewriterRulesGood.vo | 1m39.44s || +0m05.68s | +5.71% 0m40.82s | ExtractionHaskell/unsaturated_solinas | 0m37.58s || +0m03.24s | +8.62% 1m35.04s | RewriterRulesInterpGood.vo | 1m32.48s || +0m02.56s | +2.76% 0m59.49s | ExtractionHaskell/word_by_word_montgomery | 0m56.71s || +0m02.78s | +4.90% 1m45.10s | Fancy/Barrett256.vo | 1m47.00s || -0m01.90s | -1.77% 0m40.21s | p521_64.c | 0m38.97s || +0m01.24s | +3.18% 0m24.42s | SlowPrimeSynthesisExamples.vo | 0m25.67s || -0m01.25s | -4.86% 0m20.48s | secp256k1_32.c | 0m19.27s || +0m01.21s | +6.27% 1m47.10s | RewriterWf2.vo | 1m47.22s || -0m00.12s | -0.11% 0m47.85s | p521_32.c | 0m47.47s || +0m00.38s | +0.80% 0m45.66s | RewriterInterpProofs1.vo | 0m45.74s || -0m00.08s | -0.17% 0m37.18s | Fancy/Montgomery256.vo | 0m37.14s || +0m00.03s | +0.10% 0m36.26s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.14s || +0m00.11s | +0.33% 0m28.38s | ExtractionHaskell/saturated_solinas | 0m28.04s || +0m00.33s | +1.21% 0m26.80s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.83s || -0m00.02s | -0.11% 0m24.00s | RewriterWf1.vo | 0m23.96s || +0m00.03s | +0.16% 0m19.82s | ExtractionOCaml/word_by_word_montgomery | 0m20.34s || -0m00.51s | -2.55% 0m19.65s | p256_32.c | 0m19.24s || +0m00.41s | +2.13% 0m18.54s | p448_solinas_64.c | 0m19.24s || -0m00.69s | -3.63% 0m16.18s | p434_64.c | 0m16.49s || -0m00.30s | -1.87% 0m13.67s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.47s || -0m00.80s | -5.52% 0m13.22s | ExtractionOCaml/unsaturated_solinas | 0m13.72s || -0m00.50s | -3.64% 0m09.91s | p224_32.c | 0m09.89s || +0m00.01s | +0.20% 0m09.85s | ExtractionOCaml/saturated_solinas | 0m09.83s || +0m00.01s | +0.20% 0m08.66s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.86s || +0m00.79s | +10.17% 0m08.36s | p384_64.c | 0m08.46s || -0m00.10s | -1.18% 0m07.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.29s || -0m00.56s | -6.87% 0m06.66s | BoundsPipeline.vo | 0m06.73s || -0m00.07s | -1.04% 0m06.50s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.56s || -0m00.05s | -0.91% 0m06.22s | ExtractionOCaml/saturated_solinas.ml | 0m05.69s || +0m00.52s | +9.31% 0m05.50s | ExtractionHaskell/saturated_solinas.hs | 0m05.88s || -0m00.37s | -6.46% 0m03.51s | PushButtonSynthesis/Primitives.vo | 0m03.48s || +0m00.02s | +0.86% 0m03.34s | PushButtonSynthesis/SmallExamples.vo | 0m03.32s || +0m00.02s | +0.60% 0m03.31s | curve25519_32.c | 0m03.13s || +0m00.18s | +5.75% 0m03.15s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.12s || +0m00.02s | +0.96% 0m03.11s | PushButtonSynthesis/BarrettReduction.vo | 0m03.08s || +0m00.02s | +0.97% 0m02.80s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.86s || -0m00.06s | -2.09% 0m02.13s | curve25519_64.c | 0m02.02s || +0m00.10s | +5.44% 0m01.58s | p256_64.c | 0m01.66s || -0m00.07s | -4.81% 0m01.53s | p224_64.c | 0m01.60s || -0m00.07s | -4.37% 0m01.49s | secp256k1_64.c | 0m01.72s || -0m00.23s | -13.37% 0m01.34s | CLI.vo | 0m01.23s || +0m00.11s | +8.94% 0m01.16s | RewriterProofs.vo | 0m01.10s || +0m00.05s | +5.45% 0m01.16s | StandaloneOCamlMain.vo | 0m01.13s || +0m00.03s | +2.65% 0m01.10s | CompilersTestCases.vo | 0m01.09s || +0m00.01s | +0.91% 0m01.07s | StandaloneHaskellMain.vo | 0m01.04s || +0m00.03s | +2.88%
* Fix unfolding of pattern.base.lookup_defaultGravatar Jason Gross2019-03-05
|
* Fix an issue with a proof from the previous commitGravatar Jason Gross2019-03-04
| | | | | Also move lam_type_of_list to Rewriter (in prep for reifying rewrite rules).
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
| | | | This is needed to reify statements for the rewriter.
* Insert casts before literals during bounds analysisGravatar Jason Gross2019-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unless we explicitly say not to. The ability to explicitly say not to is required for, e.g., eta-expansion where we want to replace variable lists of known length with with cons cells indexing into the variable list, but don't want to pollute the code with casts. Uniformity in this way allows rewrite rules to not blow up exponentially (in the number of wildcards); we previously required a separate rewrite rule for each way of choosing between wildcard and literal. To preserve output of the pipeline, we add another pass that just strips the casts off of literals at the end. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 20m27.24s | Total | 22m39.70s || -2m12.46s | -9.74% -------------------------------------------------------------------------------------------- 0m44.27s | Rewriter.vo | 2m11.58s || -1m27.31s | -66.35% 1m15.23s | RewriterRulesInterpGood.vo | 1m50.28s || -0m35.04s | -31.78% 1m40.19s | RewriterRulesGood.vo | 1m58.05s || -0m17.85s | -15.12% 0m26.99s | AbstractInterpretationProofs.vo | 0m16.91s || +0m10.07s | +59.60% 3m15.98s | p384_32.c | 3m07.78s || +0m08.19s | +4.36% 0m42.52s | ExtractionHaskell/word_by_word_montgomery | 0m44.60s || -0m02.07s | -4.66% 0m28.63s | ExtractionHaskell/unsaturated_solinas | 0m31.38s || -0m02.75s | -8.76% 0m21.76s | ExtractionHaskell/saturated_solinas | 0m24.56s || -0m02.79s | -11.40% 0m09.87s | ExtractionOCaml/unsaturated_solinas | 0m11.28s || -0m01.41s | -12.50% 1m59.22s | RewriterWf2.vo | 2m00.09s || -0m00.87s | -0.72% 1m07.03s | Fancy/Montgomery256.vo | 1m07.31s || -0m00.28s | -0.41% 0m52.60s | Fancy/Barrett256.vo | 0m53.16s || -0m00.55s | -1.05% 0m48.17s | RewriterInterpProofs1.vo | 0m48.72s || -0m00.54s | -1.12% 0m40.16s | AbstractInterpretationWf.vo | 0m40.23s || -0m00.07s | -0.17% 0m38.35s | p521_32.c | 0m38.26s || +0m00.09s | +0.23% 0m31.56s | p521_64.c | 0m31.53s || +0m00.02s | +0.09% 0m24.64s | RewriterWf1.vo | 0m24.01s || +0m00.62s | +2.62% 0m23.54s | AbstractInterpretationZRangeProofs.vo | 0m23.64s || -0m00.10s | -0.42% 0m23.48s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.26s || +0m00.21s | +0.94% 0m20.92s | SlowPrimeSynthesisExamples.vo | 0m20.62s || +0m00.30s | +1.45% 0m19.92s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s || +0m00.12s | +0.60% 0m16.60s | ExtractionOCaml/word_by_word_montgomery | 0m17.56s || -0m00.95s | -5.46% 0m14.72s | p448_solinas_64.c | 0m14.66s || +0m00.06s | +0.40% 0m13.70s | secp256k1_32.c | 0m13.45s || +0m00.25s | +1.85% 0m13.68s | p256_32.c | 0m13.33s || +0m00.34s | +2.62% 0m13.28s | CStringification.vo | 0m13.26s || +0m00.01s | +0.15% 0m11.88s | p484_64.c | 0m11.74s || +0m00.14s | +1.19% 0m09.96s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.24s || -0m00.27s | -2.73% 0m07.47s | ExtractionOCaml/saturated_solinas | 0m07.93s || -0m00.46s | -5.80% 0m06.78s | BoundsPipeline.vo | 0m05.96s || +0m00.82s | +13.75% 0m06.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.03s || -0m00.31s | -4.40% 0m06.38s | p224_32.c | 0m06.54s || -0m00.16s | -2.44% 0m06.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s || -0m00.12s | -2.05% 0m05.45s | p384_64.c | 0m05.18s || +0m00.27s | +5.21% 0m04.82s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.84s || -0m00.01s | -0.41% 0m04.80s | ExtractionOCaml/saturated_solinas.ml | 0m05.07s || -0m00.27s | -5.32% 0m03.83s | ExtractionHaskell/saturated_solinas.hs | 0m04.07s || -0m00.24s | -5.89% 0m03.30s | PushButtonSynthesis/Primitives.vo | 0m03.31s || -0m00.01s | -0.30% 0m03.26s | PushButtonSynthesis/SmallExamples.vo | 0m03.24s || +0m00.01s | +0.61% 0m03.08s | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.96s || +0m00.12s | +4.05% 0m02.16s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.00% 0m01.57s | curve25519_64.c | 0m01.47s || +0m00.10s | +6.80% 0m01.40s | CLI.vo | 0m01.32s || +0m00.07s | +6.06% 0m01.27s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.19s || +0m00.08s | +6.72% 0m01.26s | StandaloneHaskellMain.vo | 0m01.18s || +0m00.08s | +6.77% 0m01.22s | PushButtonSynthesis/BarrettReduction.vo | 0m01.29s || -0m00.07s | -5.42% 0m01.13s | RewriterProofs.vo | 0m01.10s || +0m00.02s | +2.72% 0m01.10s | secp256k1_64.c | 0m01.01s || +0m00.09s | +8.91% 0m01.08s | StandaloneOCamlMain.vo | 0m01.13s || -0m00.04s | -4.42% 0m01.06s | p256_64.c | 0m01.02s || +0m00.04s | +3.92% 0m01.05s | AbstractInterpretation.vo | 0m01.00s || +0m00.05s | +5.00% 0m01.00s | CompilersTestCases.vo | 0m01.08s || -0m00.08s | -7.40% 0m01.00s | p224_64.c | 0m01.00s || +0m00.00s | +0.00%
* Remove an unused argumentGravatar Jason Gross2019-02-01
|
* Uncps unify_extractedGravatar Jason Gross2019-02-01
| | | | We never used the cps form, and this form is easier to read.
* Constant-propogate 0+x and x+0 after boundsGravatar Jason Gross2019-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43% -------------------------------------------------------------------------------------------- 4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88% 3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68% 2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22% 1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27% 1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01% 1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77% 0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34% 0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63% 0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25% 0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73% 0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80% 0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28% 0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28% 0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45% 0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75% 0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35% 0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77% 0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37% 0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09% 0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12% 0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73% 0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63% 0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18% 0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32% 0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93% 0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40% 0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73% 0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88% 0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16% 0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35% 0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58% 0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78% 0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22% 0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00%
* Add a rewrite rule to collapse constant castsGravatar Jason Gross2019-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If, e.g., we know from bounds analysis that the result of an operation fits in the range r[0~>0], we now just replace it with the literal constant. Fixes #493 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05% -------------------------------------------------------------------------------------------- 4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23% 3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11% 2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28% 1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42% 1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31% 1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20% 0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06% 0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38% 0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38% 0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39% 0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65% 0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49% 0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11% 0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75% 0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35% 0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94% 0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00% 0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09% 0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08% 0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39% 0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42% 0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59% 0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50% 0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33% 0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75% 0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57% 0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40% 0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49% 0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45% 0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33% 0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74% 0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73% 0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00% 0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14% 0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43%
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 10:53:15 +0000