From: Loup Vaillant Date: Mon, 6 Feb 2023 13:02:57 +0000 (+0100) Subject: Add carry propagation tests to main tests & CI X-Git-Url: https://git.codecow.com/?a=commitdiff_plain;h=73de8bdaa6625bec0440340e3dd94a0123a3508d;p=Monocypher.git Add carry propagation tests to main tests & CI --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 756e817..80edc0c 100644 --- 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 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 a630eab..90eb6ac 100755 --- 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 +# 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 7d2207d..223391f 100755 --- 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