Add --fancy-and-powerful-but-exponentially-slow-bounds-analysis test

mit-plv · Jan 4, 2024 · d04cd90 · d04cd90
1 parent 520b931
commit d04cd90
Show file tree

Hide file tree

Showing 12 changed files with 17 additions and 13 deletions.
diff --git a/Makefile.examples b/Makefile.examples
@@ -108,9 +108,13 @@ INVALID_GO_BASE_FILES := $(BASE_FILES_NEEDING_INT128)
 GO_EXTRA_UNSATURATED_SOLINAS_FUNCTIONS := carry_add carry_sub carry_opp
 GO_EXTRA_WORD_BY_WORD_MONTGOMERY_FUNCTIONS :=
 
+# We add a test for --fancy-and-powerful-but-exponentially-slow-bounds-analysis so that it's not dead code.
+# It doesn't really matter which curve we add this flag to, as long as it's fast.
+FANCY_BOUNDS_ANALYSIS_FLAG := --fancy-and-powerful-but-exponentially-slow-bounds-analysis
+
 $(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))
-$(eval $(call add_curve_keys,poly1305_32,UNSATURATED_SOLINAS,'poly1305',32,'(auto)' '2^130 - 5',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
+$(eval $(call add_curve_keys,poly1305_64,UNSATURATED_SOLINAS,'poly1305',64,'3' '2^130 - 5' $(FANCY_BOUNDS_ANALYSIS_FLAG),$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
+$(eval $(call add_curve_keys,poly1305_32,UNSATURATED_SOLINAS,'poly1305',32,'(auto)' '2^130 - 5' $(FANCY_BOUNDS_ANALYSIS_FLAG),$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p521_$(bw),UNSATURATED_SOLINAS,'p521',$(bw),'(auto)' '2^521 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS)))
 ## 2^224 - 2^96 + 1 ## does not bounds check
 #$(eval $(call add_curve_keys,p224_solinas_64,UNSATURATED_SOLINAS,'p224',64,'4' '2^224 - 2^96 + 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))

diff --git a/fiat-bedrock2/src/poly1305_32.c b/fiat-bedrock2/src/poly1305_32.c
diff --git a/fiat-bedrock2/src/poly1305_64.c b/fiat-bedrock2/src/poly1305_64.c
diff --git a/fiat-c/src/poly1305_32.c b/fiat-c/src/poly1305_32.c
diff --git a/fiat-c/src/poly1305_64.c b/fiat-c/src/poly1305_64.c
diff --git a/fiat-go/32/poly1305/poly1305.go b/fiat-go/32/poly1305/poly1305.go
diff --git a/fiat-go/64/poly1305/poly1305.go b/fiat-go/64/poly1305/poly1305.go
diff --git a/fiat-java/src/FiatPoly1305.java b/fiat-java/src/FiatPoly1305.java
diff --git a/fiat-rust/src/poly1305_32.rs b/fiat-rust/src/poly1305_32.rs
diff --git a/fiat-rust/src/poly1305_64.rs b/fiat-rust/src/poly1305_64.rs
diff --git a/fiat-zig/src/poly1305_32.zig b/fiat-zig/src/poly1305_32.zig
diff --git a/fiat-zig/src/poly1305_64.zig b/fiat-zig/src/poly1305_64.zig