diff options
author | 2018-03-31 21:45:38 -0400 | |
---|---|---|
committer | 2018-04-01 16:33:52 -0400 | |
commit | cf656c99e039786c3f4b45e1a7f64b6c8d8b7587 (patch) | |
tree | c9d1079dec7000071accb8cac5baf130015811d7 /src | |
parent | 71f76e63affede043cf79601977e844757fff522 (diff) |
Add two examples of using the pipeline in a one-liner
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 949a46aab..a2d9f7a3d 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -6875,6 +6875,23 @@ Goal False. Abort. *) + +Time Compute + (Pipeline.BoundsPipeline_full + true (relax_zrange_gen [64; 128]) + ltac:(let r := Reify (to_associational (weight 51 1) 5) in + exact r) + ZRange.type.option.None ZRange.type.option.None). + +(* N.B. When the uncurrying PR lands, we will no longer need to + manually uncurry this function example before reification *) +Time Compute + (Pipeline.BoundsPipeline_full + true (relax_zrange_gen [64; 128]) + ltac:(let r := Reify (fun '(x, y) => scmul (weight 51 1) 5 x y) in + exact r) + ZRange.type.option.None ZRange.type.option.None). + Module X25519_64. Definition n := 5%nat. Definition s := 2^255. |