diff options
| author |  jadep <jadep@mit.edu> | 2019-04-02 10:13:54 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | df629a5bdec09129c8102abcc9c9623ea9be83ce (patch) | |
| tree | afa56f1cb15922c2cb2b57b6cb9cd1d752bedfc7 /src | |
| parent | 291e80d252b476870ab01becfb9cd60b885f4e53 (diff) | |
fix up imports in SmallExamples.v
Diffstat (limited to 'src')
| -rw-r--r-- | src/PushButtonSynthesis/SmallExamples.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v index f5d7d1f29..426094fd4 100644 --- a/src/PushButtonSynthesis/SmallExamples.v +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -6,6 +6,8 @@ Require Import Crypto.Util.ZRange. Require Import Crypto.Language. Require Import Crypto.CStringification. Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Primitives. Require Import Crypto.BoundsPipeline. Import ListNotations. Local Open Scope Z_scope. Local Open Scope list_scope. @@ -45,7 +47,7 @@ Compute (Pipeline.BoundsPipelineToString true "fiat_" "fiat_mulx_u64" true None [64; 128] - ltac:(let r := Reify (Arithmetic.mulx 64) in + ltac:(let r := Reify (mulx 64) in exact r) (fun _ _ => []) (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange @@ -55,7 +57,7 @@ Compute (Pipeline.BoundsPipelineToString true "fiat_" "fiat_addcarryx_u64" true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.addcarryx 64) in + ltac:(let r := Reify (addcarryx 64) in exact r) (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange @@ -65,7 +67,7 @@ Compute (Pipeline.BoundsPipelineToString true "fiat_" "fiat_addcarryx_u51" true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.addcarryx 51) in + ltac:(let r := Reify (addcarryx 51) in exact r) (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange @@ -75,7 +77,7 @@ Compute (Pipeline.BoundsPipelineToString true "fiat_" "fiat_subborrowx_u64" true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.subborrowx 64) in + ltac:(let r := Reify (subborrowx 64) in exact r) (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange @@ -84,7 +86,7 @@ Compute (Pipeline.BoundsPipelineToString true "fiat_" "fiat_subborrowx_u51" true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.subborrowx 51) in + ltac:(let r := Reify (subborrowx 51) in exact r) (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange @@ -94,7 +96,7 @@ Compute (Pipeline.BoundsPipelineToString true "fiat_" "fiat_cmovznz64" true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.cmovznz 64) in + ltac:(let r := Reify (cmovznz 64) in exact r) (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange |