Add carry propagation tests to main tests & CI

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 756e8171364ace5465591d15e07903ac6a94de39..80edc0c5d427b8bd82a35850b64eb3135234bbee 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -102,12 +102,10 @@ jobs:
         run: make clean && make tis-ci -j4
 
       - name: Run speed tests
-        run: |
-          make clean && make speed -j4
+        run: make clean && make speed -j4
 
       - name: Run code coverage tests
-        run: |
-          ./tests/coverage.sh
+        run: ./tests/coverage.sh
 
       - name: Run tests with clang sanitizers
         run: |
@@ -162,3 +160,6 @@ jobs:
           echo
           echo "All valgrind tests passed!"
           echo
+
+      - name: Check bignum arithmetic
+        run: tests/proofs/test_carry.sh

diff --git a/tests/proofs/filter.sh b/tests/proofs/filter.sh
deleted file mode 100755 (executable)
index ca7bbcf..0000000
--- a/tests/proofs/filter.sh
+++ /dev/null
@@ -1,23 +0,0 @@
-#! /bin/env sh
-
-echo "#! /bin/env python3"
-echo "from overflow import *"
-echo ""
-sed -n "/PROOF $1/,/CQFD $1/p"                                          |\
-    sed '1d;$d'                                                         |\
-    sed 's|    ||'                                                         |\
-    sed 's|//- ||'                                                      |\
-    sed 's|^.*//-.*$||'                                                 |\
-    sed 's|  *//.*||'                                                   |\
-    sed 's|//|#|'                                                       |\
-    sed 's|const ||'                                                    |\
-    sed 's|;||'                                                         |\
-    sed 's|ctx->|ctx_|'                                                 |\
-    sed 's|\[|_|g'                                                      |\
-    sed 's|\]||g'                                                       |\
-    sed 's|(\([a-zA-Z0-9_]*\))\([a-zA-Z0-9_]*\)|\1(\2)|g'               |\
-    sed 's|^\([a-zA-Z0-9_]*\) \([a-zA-Z0-9_]*\) = \(.*\)$|\2 = \1(\3)|' |\
-    sed 's|\* \([0-9][0-9]*\)|\* cast(\1)|g'                            |\
-    sed 's|\+ \([0-9][0-9]*\)|\+ cast(\1)|g'                            |\
-    sed 's|\- \([0-9][0-9]*\)|\- cast(\1)|g'                            |\
-    cat

diff --git a/tests/proofs/test_carry.sh b/tests/proofs/test_carry.sh
index a630eabbc9933f3d675f3f90fbc3ec988109de3f..90eb6ac0638b02590ab02be23af0fce3df3de5a1 100755 (executable)
--- a/tests/proofs/test_carry.sh
+++ b/tests/proofs/test_carry.sh
@@ -1,4 +1,55 @@
-#! /bin/env sh
+#! /bin/sh
+
+# This file is dual-licensed.  Choose whichever licence you want from
+# the two licences listed below.
+#
+# The first licence is a regular 2-clause BSD licence.  The second licence
+# is the CC-0 from Creative Commons. It is intended to release Monocypher
+# to the public domain.  The BSD licence serves as a fallback option.
+#
+# SPDX-License-Identifier: BSD-2-Clause OR CC0-1.0
+#
+# ------------------------------------------------------------------------
+#
+# Copyright (c) 2023, Loup Vaillant
+# All rights reserved.
+#
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are
+# met:
+#
+# 1. Redistributions of source code must retain the above copyright
+#    notice, this list of conditions and the following disclaimer.
+#
+# 2. Redistributions in binary form must reproduce the above copyright
+#    notice, this list of conditions and the following disclaimer in the
+#    documentation and/or other materials provided with the
+#    distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+# HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+# DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+# THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+# (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# ------------------------------------------------------------------------
+#
+# Written in 2023 by Loup Vaillant
+#
+# To the extent possible under law, the author(s) have dedicated all copyright
+# and related neighboring rights to this software to the public domain
+# worldwide.  This software is distributed without any warranty.
+#
+# You should have received a copy of the CC0 Public Domain Dedication along
+# with this software.  If not, see
+# <https://creativecommons.org/publicdomain/zero/1.0/>
 
 set -e
 
@@ -7,7 +58,32 @@ DIR=$(dirname "$0")
 POLY=$DIR/poly1305.gen.py
 
 echo "Check limb overflow: $POLY"
-$DIR/filter.sh Poly1305 <$DIR/../../src/monocypher.c >$POLY
+
+# Turn Poly1305 C code into Python code
+echo "#! /bin/env python3"     >$POLY
+echo "from overflow import *" >>$POLY
+echo ""                       >>$POLY
+cat $DIR/../../src/monocypher.c                                         |\
+    sed -n "/PROOF Poly1305 /,/CQFD Poly1305 /p"                        |\
+    sed '1d;$d'                                                         |\
+    sed 's|    ||'                                                         |\
+    sed 's|//- ||'                                                      |\
+    sed 's|^.*//-.*$||'                                                 |\
+    sed 's|  *//.*||'                                                   |\
+    sed 's|//|#|'                                                       |\
+    sed 's|const ||'                                                    |\
+    sed 's|;||'                                                         |\
+    sed 's|ctx->|ctx_|'                                                 |\
+    sed 's|\[|_|g'                                                      |\
+    sed 's|\]||g'                                                       |\
+    sed 's|(\([a-zA-Z0-9_]*\))\([a-zA-Z0-9_]*\)|\1(\2)|g'               |\
+    sed 's|^\([a-zA-Z0-9_]*\) \([a-zA-Z0-9_]*\) = \(.*\)$|\2 = \1(\3)|' |\
+    sed 's|\* \([0-9][0-9]*\)|\* cast(\1)|g'                            |\
+    sed 's|\+ \([0-9][0-9]*\)|\+ cast(\1)|g'                            |\
+    sed 's|\- \([0-9][0-9]*\)|\- cast(\1)|g'                            |\
+    cat >>$POLY
+
+# Run self-checking Python code
 python3 $DIR/poly1305.gen.py
 
 echo "No limb overflow detected"

diff --git a/tests/test.sh b/tests/test.sh
index 7d2207d4129f0059a46fff8bdf9060010e2bff8f..223391f0283775cf401907353f20d64a39af9815 100755 (executable)
--- a/tests/test.sh
+++ b/tests/test.sh
@@ -64,3 +64,5 @@ make clean;  make test.out;  valgrind ./test.out
 echo
 echo "All sanitisers passed!"
 echo
+
+tests/proofs/test_carry.sh