Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added dettman multiplication algorithm, made changes to equivalence checker #1481

Closed
wants to merge 20 commits into from
Closed

Added dettman multiplication algorithm, made changes to equivalence checker #1481

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
9932da7
Added first draft of bitcoin multiplication algorithm (no intermediat…
OwenConoly Jul 1, 2022
a36c987
Fixed problem with redundant bit shift in generated C code for bitcoi…
OwenConoly Jul 1, 2022
87bef55
Added c file containing code that results from compiling bitcoin mulm…
OwenConoly Jul 9, 2022
8535414
Made generalized bitcoin mulmod algorithm work with compiler (previou…
OwenConoly Jul 10, 2022
aa0ae88
Proved general form of bitcoin mulmod algorithm. Added appropriate h…
OwenConoly Jul 10, 2022
e1dba05
Split up files in BitcoinMultiplication folder. Added test of genera…
OwenConoly Jul 10, 2022
cbce82a
Added bitcoin multiplication command line interface. Bitcoin multipl…
OwenConoly Jul 13, 2022
0a07c99
Refactored HelpfulFunctions.v (split into Core.v and ListUtil.v). Re…
OwenConoly Jul 25, 2022
f022b68
Renamed files, modules, etc: BitcoinMultiplication -> DettmanMultipli…
OwenConoly Jul 25, 2022
dc28b2e
Added files containing failed attempt to compile dettman multiplicati…
OwenConoly Jul 28, 2022
c6e672d
Fixed DettmanMultipliction-to-Bedrock2 compiling issue. Modified ass…
OwenConoly Jul 29, 2022
26f9d57
Renamed generated files for secp256k1: secp256k1 -> secp256k1_montgom…
OwenConoly Jul 30, 2022
c68ba34
Cleaned things up; removed unwanted files; added cli documentation; a…
OwenConoly Jul 30, 2022
6daa391
reordered steps (which commute) in dettman mul algorithm. Purely aes…
OwenConoly Aug 6, 2022
13bd067
Removed assembly file that didn't belong.
OwenConoly Sep 1, 2022
1019f08
Fixed bug with limbwidth, limb-number guessing for dettman multiplica…
OwenConoly Sep 1, 2022
9c13d04
added addcarry rewriting rule to assembly equivalence checker
OwenConoly Sep 1, 2022
f635643
added or-to-add rewriting; better bounds analysis to assembly checker
OwenConoly Sep 9, 2022
ffff318
mostly implemented cli option to use optional rewrite rule. proof al…
OwenConoly Nov 4, 2022
56d0027
added command line option to turn on optional rewriting rules for ass…
OwenConoly Nov 5, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,7 @@ third_party/openssl-nistz256-amd64/measure
third_party/openssl-nistz256/measure
third_party/curve25519-donna-c64/measure
src/ExtractionHaskell/saturated_solinas
src/ExtractionHaskell/dettman_multiplication
src/ExtractionHaskell/unsaturated_solinas
src/ExtractionHaskell/word_by_word_montgomery
src/ExtractionHaskell/base_conversion
Expand All @@ -193,14 +194,17 @@ src/ExtractionHaskell/*.hi
src/ExtractionHaskell/*.hs
src/ExtractionHaskell/*.o
src/ExtractionOCaml/saturated_solinas
src/ExtractionOCaml/dettman_multiplication
src/ExtractionOCaml/unsaturated_solinas
src/ExtractionOCaml/word_by_word_montgomery
src/ExtractionOCaml/base_conversion
src/ExtractionOCaml/bedrock2_saturated_solinas
src/ExtractionOCaml/bedrock2_dettman_multiplication
src/ExtractionOCaml/bedrock2_unsaturated_solinas
src/ExtractionOCaml/bedrock2_word_by_word_montgomery
src/ExtractionOCaml/bedrock2_base_conversion
src/ExtractionOCaml/with_bedrock2_saturated_solinas
src/ExtractionOCaml/with_bedrock2_dettman_multiplication
src/ExtractionOCaml/with_bedrock2_unsaturated_solinas
src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery
src/ExtractionOCaml/with_bedrock2_base_conversion
Expand Down
15 changes: 11 additions & 4 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -269,17 +269,21 @@ endef
UNSATURATED_SOLINAS_FUNCTIONS := carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
FUNCTIONS_FOR_25519 := $(UNSATURATED_SOLINAS_FUNCTIONS) carry_scmul121666
WORD_BY_WORD_MONTGOMERY_FUNCTIONS := mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
DETTMAN_MULTIPLICATION_FUNCTIONS := mul
UNSATURATED_SOLINAS := src/ExtractionOCaml/unsaturated_solinas
WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/word_by_word_montgomery
DETTMAN_MULTIPLICATION := src/ExtractionOCaml/dettman_multiplication

UNSATURATED_SOLINAS_BASE_FILES := # p224_solinas_64
WORD_BY_WORD_MONTGOMERY_BASE_FILES := # p434_32
ALL_BASE_FILES := $(UNSATURATED_SOLINAS_BASE_FILES) $(WORD_BY_WORD_MONTGOMERY_BASE_FILES)
DETTMAN_MULTIPLICATION_BASE_FILES :=
ALL_BASE_FILES := $(UNSATURATED_SOLINAS_BASE_FILES) $(WORD_BY_WORD_MONTGOMERY_BASE_FILES) $(DETTMAN_MULTIPLICATION_BASE_FILES)

BASE_FILES_NEEDING_INT128 := p448_solinas_32

GO_EXTRA_UNSATURATED_SOLINAS_FUNCTIONS := carry_add carry_sub carry_opp
GO_EXTRA_WORD_BY_WORD_MONTGOMERY_FUNCTIONS :=
GO_EXTRA_DETTMAN_MULTIPLICATION_FUNCTIONS :=

$(foreach bw,64 32,$(eval $(call add_curve_keys,curve25519_$(bw),UNSATURATED_SOLINAS,'25519',$(bw),'(auto)' '2^255 - 19',$(FUNCTIONS_FOR_25519),UNSATURATED_SOLINAS)))
$(eval $(call add_curve_keys,poly1305_64,UNSATURATED_SOLINAS,'poly1305',64,'3' '2^130 - 5',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
Expand All @@ -290,15 +294,17 @@ $(eval $(call add_curve_keys,p521_64,UNSATURATED_SOLINAS,'p521',64,'9' '2^521 -
$(eval $(call add_curve_keys,p448_solinas_64,UNSATURATED_SOLINAS,'p448',64,'8' '2^448 - 2^224 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
$(eval $(call add_curve_keys,p448_solinas_32,UNSATURATED_SOLINAS,'p448',32,'16' '2^448 - 2^224 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
$(foreach bw,64 32,$(eval $(call add_curve_keys,p256_$(bw),WORD_BY_WORD_MONTGOMERY,'p256',$(bw),'2^256 - 2^224 + 2^192 + 2^96 - 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1',$(bw),'2^256 - 2^32 - 977',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_montgomery_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1_montgomery',$(bw),'2^256 - 2^32 - 977',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,p384_$(bw),WORD_BY_WORD_MONTGOMERY,'p384',$(bw),'2^384 - 2^128 - 2^96 + 2^32 - 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,p224_$(bw),WORD_BY_WORD_MONTGOMERY,'p224',$(bw),'2^224 - 2^96 + 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64,$(eval $(call add_curve_keys,p434_$(bw),WORD_BY_WORD_MONTGOMERY,'p434',$(bw),'2^216 * 3^137 - 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY))) # 32 is a bit too heavy

$(foreach bw,64 32,$(eval $(call add_curve_keys,curve25519_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'25519_scalar',$(bw),'2^252 + 27742317777372353535851937790883648493',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,p256_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'p256_scalar',$(bw),'2^256 - 2^224 + 2^192 - 89188191075325690597107910205041859247',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,p384_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'p384_scalar',$(bw),'2^384 - 1388124618062372383947042015309946732620727252194336364173',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1_scalar',$(bw),'2^256 - 432420386565659656852420866394968145599',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_montgomery_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1_montgomery_scalar',$(bw),'2^256 - 432420386565659656852420866394968145599',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))

$(foreach bw,64,$(eval $(call add_curve_keys,secp256k1_dettman_$(bw),DETTMAN_MULTIPLICATION,'secp256k1_dettman',$(bw),5 52 '2^256 - 4294968273' 1,$(DETTMAN_MULTIPLICATION_FUNCTIONS),DETTMAN_MULTIPLICATION)))

# Files taking 30s or less
LITE_BASE_FILES := curve25519_64 poly1305_64 poly1305_32 p256_64 secp256k1_64 p384_64 p224_32 p434_64 p448_solinas_64 secp256k1_32 p256_32 p448_solinas_32 \
Expand All @@ -325,6 +331,7 @@ LITE_ZIG_FILES := $(patsubst %,$(ZIG_DIR)%.zig,$(LITE_BASE_FILES))

BEDROCK2_UNSATURATED_SOLINAS := src/ExtractionOCaml/bedrock2_unsaturated_solinas
BEDROCK2_WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/bedrock2_word_by_word_montgomery
BEDROCK2_DETTMAN_MULTIPLICATION := src/ExtractionOCaml/bedrock2_dettman_multiplication

C_EXTRA_ARGS := --inline --static --use-value-barrier

Expand Down Expand Up @@ -581,7 +588,7 @@ Makefile.coq: Makefile _CoqProject
$(HIDE)$(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = $(INSTALLDEFAULTROOT) -o Makefile-coq && cat Makefile-coq | sed 's/^printenv:/printenv::/g; s/^printenv:::/printenv::/g; s/^all:/all-old:/g; s/^validate:/validate-vo:/g; s/^.PHONY: validate/.PHONY: validate-vo/g' > $@ && rm -f Makefile-coq


BASE_STANDALONE := unsaturated_solinas saturated_solinas word_by_word_montgomery base_conversion
BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion
BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE))
STANDALONE := $(BASE_STANDALONE)
ifneq ($(SKIP_BEDROCK2),1)
Expand Down
3 changes: 3 additions & 0 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ src/Arithmetic/BYInv.v
src/Arithmetic/BarrettReduction.v
src/Arithmetic/BaseConversion.v
src/Arithmetic/Core.v
src/Arithmetic/DettmanMultiplication.v
src/Arithmetic/FLia.v
src/Arithmetic/FancyMontgomeryReduction.v
src/Arithmetic/Freeze.v
Expand Down Expand Up @@ -193,6 +194,8 @@ src/PushButtonSynthesis/BarrettReduction.v
src/PushButtonSynthesis/BarrettReductionReificationCache.v
src/PushButtonSynthesis/BaseConversion.v
src/PushButtonSynthesis/BaseConversionReificationCache.v
src/PushButtonSynthesis/DettmanMultiplication.v
src/PushButtonSynthesis/DettmanMultiplicationReificationCache.v
src/PushButtonSynthesis/FancyMontgomeryReduction.v
src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
src/PushButtonSynthesis/InvertHighLow.v
Expand Down
Loading