blob: a0d2d3528f50080cd87b6d990dbaf46f7071437a (
plain)
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
|
(* This file is autogenerated from Karatsuba.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Karatsuba.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Ltac add_mul_sig pkg :=
if_goldilocks
pkg
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let half_sz := Tag.get pkg TAG.half_sz in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let mul_sig := fresh "mul_sig" in
let mul_sig := pose_mul_sig sz m wt s c half_sz wt_nonzero mul_sig in
Tag.update pkg TAG.mul_sig mul_sig)
ltac:(fun _ => pkg)
().
Ltac add_square_sig pkg :=
if_goldilocks
pkg
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let mul_sig := Tag.get pkg TAG.mul_sig in
let square_sig := fresh "square_sig" in
let square_sig := pose_square_sig sz m wt mul_sig square_sig in
Tag.update pkg TAG.square_sig square_sig)
ltac:(fun _ => pkg)
().
Ltac add_Karatsuba_package pkg :=
let pkg := add_mul_sig pkg in
let pkg := add_square_sig pkg in
Tag.strip_local pkg.
Module MakeKaratsubaPackage (PKG : PrePackage).
Module Import MakeKaratsubaPackageInternal := MakePackageBase PKG.
End MakeKaratsubaPackage.
|
