Support for large finite fields #851
Labels
Comments
|
Unfortunately, the synthesis time of the current code seems to be exponential in the number of limbs (for WBW Montgomery) or at least cubic (for unsaturated Solinas), for unclear reasons. Our 12-limb example takes around 8 minutes, and just a couple more limbs brings us up to an hour. 3072-bit primes on 64-bit machines would involve 48 limbs, which is much more than the code can handle at this point. There are two issues, here:
Super-linear time in positional->associational->positional: CodeRequire Import Coq.Lists.List Coq.ZArith.ZArith.
Require Import Crypto.ArithmeticCPS.Core.
Require Import Crypto.ArithmeticCPS.ModOps.
Import ListNotations.
Open Scope Z_scope.
Open Scope nat_scope.
Open Scope list_scope.
Module RT_ExtraAx := Core.RT_Extra Core.RuntimeAxioms.
Module ModOpsAx := ModOps.ModOps Core.RuntimeAxioms.
Module PositionalAx := ArithmeticCPS.Core.Positional Core.RuntimeAxioms.
Definition test (nlimbs : nat) (f : list Z) : list Z
:= let wt := weight 64 1 in
let p := PositionalAx.to_associational wt nlimbs (RT_ExtraAx.expand_list 0%Z f nlimbs) in
PositionalAx.from_associational_cps wt nlimbs p _ id.
Import RuntimeAxioms.
Ltac timetest n := idtac "n=" n; time (idtac; let x := (eval vm_compute in (test n)) in idtac).
Ltac timetest_up_to n :=
lazymatch n with
| O => idtac
| S ?n => timetest_up_to n
end;
timetest n.
Goal True. timetest_up_to 35. Abort.Table of timing as a function of limbs
Super-linear time in chained-carries: CodeRequire Import Coq.Lists.List Coq.ZArith.ZArith.
Require Import Crypto.ArithmeticCPS.Core.
Require Import Crypto.ArithmeticCPS.ModOps.
Require Crypto.UnsaturatedSolinasHeuristics.
Import ListNotations.
Open Scope Z_scope.
Open Scope nat_scope.
Open Scope list_scope.
Module RT_ExtraAx := Core.RT_Extra Core.RuntimeAxioms.
Module ModOpsAx := ModOps.ModOps Core.RuntimeAxioms.
Module PositionalAx := ArithmeticCPS.Core.Positional Core.RuntimeAxioms.
Definition test2 (nlimbs : nat) (f : list Z) : list Z
:= let wt := weight 64 1 in
let s := (2^(64 * Z.of_nat nlimbs - 1))%Z in
let c := [(1, 1)]%Z in
let idxs := UnsaturatedSolinasHeuristics.carry_chains nlimbs s c in
let p := PositionalAx.chained_carries_cps wt nlimbs s c (RT_ExtraAx.expand_list 0%Z f nlimbs) idxs _ id in
p.
Import RuntimeAxioms.
Ltac timetest2 n :=
idtac "n=" n;
restart_timer;
let x := (eval vm_compute in (test2 n)) in
finish_timing ("Tactic call vm_compute");
restart_timer;
let x := (eval vm_compute in x) in
finish_timing ("Tactic call noop-vm_compute").
Ltac timetest2_up_to n :=
lazymatch n with
| O => idtac
| S ?n => timetest2_up_to n
end;
timetest2 n.
Goal True. timetest2_up_to 15. Abort.Table of timing as a function of limbs
Super-linear time in WBW Montgomery multiplication: CodeRequire Import Coq.Lists.List Coq.ZArith.ZArith.
Require Import Crypto.ArithmeticCPS.Core.
Require Import Crypto.ArithmeticCPS.ModOps.
Require Import Crypto.ArithmeticCPS.WordByWordMontgomery.
Require Import Crypto.Util.ZUtil.ModInv.
Import ListNotations.
Open Scope Z_scope.
Open Scope nat_scope.
Open Scope list_scope.
Module Import RT_ExtraAx := Core.RT_Extra Core.RuntimeAxioms.
Module ModOpsAx := ModOps.ModOps Core.RuntimeAxioms.
Module PositionalAx := ArithmeticCPS.Core.Positional Core.RuntimeAxioms.
Module WordByWordMontgomeryAx := ArithmeticCPS.WordByWordMontgomery.WordByWordMontgomery Core.RuntimeAxioms.
Definition test3 (nlimbs : nat) (f g : list Z) : list Z
:= let wt := weight 64 1 in
let m := (2^(64 * Z.of_nat nlimbs - 1) - 1)%Z in
let m' := match Z.modinv (-m) (2^64) with
| Some m' => m'
| None => 0%Z
end in
WordByWordMontgomeryAx.mulmod 64 nlimbs m m' (expand_list 0%Z f nlimbs) (expand_list 0%Z g nlimbs).
Import RuntimeAxioms.
Ltac timetest3 n :=
idtac "n=" n;
restart_timer;
let x := (eval vm_compute in (test3 n)) in
finish_timing ("Tactic call vm_compute");
restart_timer;
let x := (eval vm_compute in x) in
finish_timing ("Tactic call noop-vm_compute").
Ltac timetest3_up_to n :=
lazymatch n with
| O => idtac
| S ?n => timetest3_up_to n
end;
timetest3 n.
Goal True. timetest3_up_to 9. Abort.Table of timing as a function of limbs
N.B. This code runs with commit 4c54bbb of our project. I expect it'll continue working for some time, but I'm leaving this commit hash here so it's easy to dig up a working version if we need to. |
|
Some additional stats on WBW Montgomery multiplication (without arithmetic simplification): CodeRequire Import Coq.Lists.List Coq.ZArith.ZArith.
Require Import Crypto.ArithmeticCPS.Core.
Require Import Crypto.ArithmeticCPS.ModOps.
Require Import Crypto.ArithmeticCPS.WordByWordMontgomery.
Require Import Crypto.Util.ZUtil.ModInv.
Import ListNotations.
Open Scope Z_scope.
Open Scope nat_scope.
Open Scope list_scope.
Module Import RT_ExtraAx := Core.RT_Extra Core.RuntimeAxioms.
Module ModOpsAx := ModOps.ModOps Core.RuntimeAxioms.
Module PositionalAx := ArithmeticCPS.Core.Positional Core.RuntimeAxioms.
Module WordByWordMontgomeryAx := ArithmeticCPS.WordByWordMontgomery.WordByWordMontgomery Core.RuntimeAxioms.
Definition test3 (nlimbs : nat) (f g : list Z) : list Z
:= let wt := weight 64 1 in
let m := (2^(64 * Z.of_nat nlimbs - 1) - 1)%Z in
let m' := match Z.modinv (-m) (2^64) with
| Some m' => m'
| None => 0%Z
end in
WordByWordMontgomeryAx.mulmod 64 nlimbs m m' (expand_list 0%Z f nlimbs) (expand_list 0%Z g nlimbs).
Import RuntimeAxioms.
Inductive tags := FORALL | FUN | LET | MATCHPAIR.
Inductive HList := Nil | Cons {A} (x : A) (y : nat) (xs : HList).
Fixpoint count (v : HList) : Z
:= match v with
| Nil => 0
| Cons A x n xs => Z.of_nat n + count xs
end%Z.
Delimit Scope hlist_scope with hlist.
Bind Scope hlist_scope with HList.
Notation "( x , y ) :: z" := (Cons x y z) (at level 60, right associativity) : hlist_scope.
Ltac count_size v acc :=
let __ := match goal with _ => idtac acc end in
let inc_count acc tag
:= lazymatch acc with
| context ACC[Cons tag ?c0]
=> let acc := context ACC[Cons tag (S c0)] in
acc
| _ => constr:(Cons tag 1%nat acc)
end in
let handle_fun v acc :=
lazymatch v with
| fun x : ?A => ?f
=> let acc := count_size A acc in
let f' := fresh in
let acc' := fresh in
lazymatch
constr:(
fun x : A
=> match f, acc return _ with
| f', acc'
=> ltac:(let f := (eval cbv delta [f'] in f') in
let acc := (eval cbv delta [acc'] in acc') in
clear f' acc';
let acc := count_size f acc in
refine acc)
end) with
| fun _ => ?acc => acc
| ?e => fail 0 "cannot eliminate functional dependencies of" e
end
| let x : ?A := ?v in ?f
=> let acc := count_size A acc in
let acc := count_size v acc in
let f' := fresh in
let acc' := fresh in
lazymatch
constr:(
let x : A := v in
match f, acc return _ with
| f', acc'
=> ltac:(let f := (eval cbv delta [f'] in f') in
let acc := (eval cbv delta [acc'] in acc') in
clear f' acc';
let acc := count_size f acc in
refine acc)
end) with
| let _ := _ in ?acc => acc
| ?e => fail 0 "cannot eliminate functional dependencies of" e
end
end in
lazymatch v with
| fun x => @?f x => let acc := inc_count acc FUN in handle_fun f acc
| forall x, @?f x => let acc := inc_count acc FORALL in handle_fun f acc
| let x := _ in _ => let acc := inc_count acc LET in handle_fun v acc
| ?f ?x => let acc := count_size f acc in
let acc := count_size x acc in
acc
| match ?x with pair a b => @?f a b end
=> let acc := inc_count acc MATCHPAIR in
let acc := count_size x acc in
handle_fun f acc
| ?v => let iv := constr:(ltac:(match goal with
| _ => is_var v; exact true
| _ => exact false
end)) in
lazymatch iv with
| true => acc
| false => inc_count acc v
end
end.
Axiom ax : forall {T}, T.
Ltac strip_fun v :=
lazymatch v with
| fun x : ?A => ?f
=> let f := lazymatch type of v with
| forall x : ?A, ?P => constr:(match @ax A as x return P with x => f end)
end in
strip_fun f
| ?v => v
end.
Ltac count_size_dlet v :=
lazymatch v with
| @Let_In ?A (fun _ => ?T) ?v (fun x => ?f)
=> let f := constr:(match @ax A return T with x => f end) in
let n := count_size_dlet f in
uconstr:(S n)
| @Let_In ?A ?P ?v (fun x => ?f)
=> let f := constr:(match @ax A as b return P b with x => f end) in
let n := count_size_dlet f in
uconstr:(S n)
| fun x : ?A => ?f
=> let f := lazymatch type of v with
| ?A -> ?T => constr:(match @ax A return T with x => f end)
| forall x : ?A, ?P => constr:(match @ax A as x return P with x => f end)
end in
let n := count_size_dlet f in
n
| _ => constr:(O)
end.
Require Ltac2.Ltac2.
Require Ltac2.Array.
Require Ltac2.Constr.
Require Ltac2.Ltac1.
Require Ltac2.Message.
Require Ltac2.Int.
Require Ltac2.Control.
Module Import WithLtac2.
Import Ltac2.Ltac2.
Import Ltac2.Constr.
Ltac2 rec count_dlet (v : constr) :=
match Unsafe.kind v with
| Unsafe.App _Let_In args
=> match Int.lt 3 (Array.length args) with
| true => Int.add 1 (count_dlet (Array.get args 3))
| false => 0
end
| Unsafe.Lambda _ _ body
=> count_dlet body
| _ => 0
end.
Ltac2 print_count_dlet (v : constr option) :=
match v with
| Some v
=> let n := count_dlet v in
Message.print (Message.concat (Message.of_string "# lets = ") (Message.of_int n))
| None => Control.zero Not_found
end.
Ltac count_dlet_ltac2 := ltac2:(v |- print_count_dlet (Ltac1.to_constr v)).
End WithLtac2.
Ltac timetest3 n :=
idtac "n=" n;
restart_timer;
let x := (eval vm_compute in (test3 n)) in
finish_timing ("Tactic call vm_compute");
restart_timer;
let x := (eval vm_compute in x) in
finish_timing ("Tactic call noop-vm_compute");
count_dlet_ltac2 x.
Ltac timetest3_up_to n :=
lazymatch n with
| O => idtac
| S ?n => timetest3_up_to n
end;
timetest3 n.
Goal True. timetest3_up_to 9. Abort.And to generate the number of lines of code in the output: for i in $(seq 1 10); do echo "$i$(printf '\t')$(./src/ExtractionOCaml/word_by_word_montgomery p 64 "2^($i*64)-1" mul --no-primitives | wc -l)"; doneTable
|
I see. Thanks for the quick and detailed response. I think then it's obviously then it's currently not interesting for us but I'll watch the issue of course. Unfortunately I don't have the resources to help. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
As far as I understand, the focus of this project is ECC, even though other uses of finite field arithmetic are supported (Poly1305). Is it easily possible to support finite fields large enough that DLog is hard in them, e.g., primes of size ~ 3072 bits?
I know the cool kids use ECC nowadays but finite field DLog is not dead either. I'm specifically asking because Bitcoin is looking into MuHash [1] for incremental hashing for sets and finite field DLog is slightly more efficient for this use case in this context [2,3]. I wonder if fiat-crypto could be useful here. Specifically the linked PR implements finite field arithmetic for 2^3072 - 1103717 but since this a new feature, the choice of the prime is not set in stone.
[1] http://cseweb.ucsd.edu/~Mihir/papers/inchash.pdf
[2] https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017-May/014337.html
[3] bitcoin/bitcoin#19055
The text was updated successfully, but these errors were encountered: