1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
(** * Push-Button Synthesis Examples *)
Require Import Coq.Strings.String.
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
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.
Import
Language.Compilers
CStringification.Compilers.
Import Compilers.defaults.
Import Associational Positional.
Time Compute
(Pipeline.BoundsPipeline
true None [64; 128]
ltac:(let r := Reify (to_associational (weight 51 1) 5) in
exact r)
(Some (repeat (@None _) 5), tt)
ZRange.type.base.option.None).
Time Compute
(Pipeline.BoundsPipeline
true None [64; 128]
ltac:(let r := Reify (scmul (weight 51 1) 5) in
exact r)
(None, (Some (repeat (@None _) 5), tt))
ZRange.type.base.option.None).
Compute
(Pipeline.BoundsPipeline
true None [64; 128]
ltac:(let r := Reify (fun f => carry_mulmod 51 1 (2^255) [(1,19)] 5 (seq 0 5 ++ [0; 1])%list%nat f f) in
exact r)
(Some (repeat (@None _) 5), tt)
ZRange.type.base.option.None).
Compute
(Pipeline.BoundsPipelineToString
true "fiat_" "fiat_mulx_u64"
true None [64; 128]
ltac:(let r := Reify (mulx 64) in
exact r)
(fun _ _ => [])
(Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange
(Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange).
Compute
(Pipeline.BoundsPipelineToString
true "fiat_" "fiat_addcarryx_u64"
true None [1; 64; 128]
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
(Some r[0~>2^64-1], Some r[0~>1])%zrange).
Compute
(Pipeline.BoundsPipelineToString
true "fiat_" "fiat_addcarryx_u51"
true None [1; 64; 128]
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
(Some r[0~>2^51-1], Some r[0~>1])%zrange).
Compute
(Pipeline.BoundsPipelineToString
true "fiat_" "fiat_subborrowx_u64"
true None [1; 64; 128]
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
(Some r[0~>2^64-1], Some r[0~>1])%zrange).
Compute
(Pipeline.BoundsPipelineToString
true "fiat_" "fiat_subborrowx_u51"
true None [1; 64; 128]
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
(Some r[0~>2^51-1], Some r[0~>1])%zrange).
Compute
(Pipeline.BoundsPipelineToString
true "fiat_" "fiat_cmovznz64"
true None [1; 64; 128]
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
(Some r[0~>2^64-1])%zrange).
|
