Add coeff_signed_to_unsigned() functions and its proof

[rod-chapman]

This PR adds only the coeff_signed_to_unsigned() function in poly.c and its proof.

This was previously added in support of the proof of poly_compress(), but that proof is blocked pending CBMC bug fixes.

This PR adds coeff_signed_to_unsigned() in isolation so that proofs of other functions may proceed, such as poly_tobytes()

To run proofs, cd to "cbmc/proofs/coeff_signed_to_unsigned", then either

1. "make" (runs with litani and cbmc-viewer)
   or
2. "make -f desktop.mk" (run with command-line CBMC tools only - best for inspecting details results.)

[cothan]

Hi @rod-chapman , If you have nix installed (https://zero-to-nix.com/start/install), you can go to the base directory and run nix develop to have identical CI environment at your local. Perhaps it helps you debug CI.

[rod-chapman]

I am running NIX locally and it works well. The proof of coeff_signed_to_unsigned() works perfectly locally, but fails everying in the GitHub runner, but I can't work out why...

[cothan]

If the upstream version is newer, maybe you need to update the new hash here:

https://github.com/pq-code-package/mlkem-c-aarch64/blob/main/flake.nix#L31

[potsrevennil]

Hi, @rod-chapman I came across this, and I observed the same issue as you. I figure it might be helpful to upload some logs and artifacts to make troubleshooting the inconsistent results between local and CI environments easier, or just produce more logs vis the python script in CI. I can do this, but I will need guidance on which files to upload to help resolve this kind of issue.

By the way, here are the errors that I extracted from the artifact I uploaded to my fork.
Hope that it would help.

    <result property=coeff_signed_to_unsigned.postcondition.1 status=ERROR>,
      <location file=mlkem/poly.h function=coeff_signed_to_unsigned line=53 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.postcondition.2 status=ERROR>,
      <location file=mlkem/poly.h function=coeff_signed_to_unsigned line=54 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.postcondition.3 status=ERROR>,
      <location file=mlkem/poly.h function=coeff_signed_to_unsigned line=55 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.assertion.1 status=ERROR>,
      <location file=mlkem/poly.c function=coeff_signed_to_unsigned line=116 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.assertion.2 status=ERROR>,
      <location file=mlkem/poly.c function=coeff_signed_to_unsigned line=117 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.overflow.1 status=ERROR>,
      <location file=mlkem/poly.h function=coeff_signed_to_unsigned line=55 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.overflow.2 status=ERROR>,
      <location file=mlkem/poly.h function=coeff_signed_to_unsigned line=55 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.overflow.3 status=ERROR>,
      <location file=mlkem/poly.c function=coeff_signed_to_unsigned line=114 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.overflow.4 status=ERROR>,
      <location file=mlkem/poly.c function=coeff_signed_to_unsigned line=114 working-directory=cbmc/proofs/>,
    </result>,
--
    <result property=coeff_signed_to_unsigned.overflow.5 status=ERROR>,
      <location file=mlkem/poly.c function=coeff_signed_to_unsigned line=120 working-directory=cbmc/proofs/>,
    </result>,

[rod-chapman]

OK... thanks for that data. If I run "make" locally (within a NIX shell), then look in the logs/result.xml file, I see things like:

<result property="coeff_signed_to_unsigned.postcondition.1" status="SUCCESS">
  <location file="/Users/rodchap/Desktop/rod/projects/crypto/pqcp/aarch64-rod-main/mlkem/poly.h" function="coeff_signed_to_unsigned" line="53" working-directory="/Users/rodchap/Desktop/rod/projects/crypto/pqcp/aarch64-rod-main/cbmc/proofs/coeff_signed_to_unsigned"/>
</result>

which shows the same proofs succeeding. Still no idea why they are failing in CI... :-(

[mkannwischer]

I ran this locally on my x86 machine as well as on a M1 MacMini.
On x86 all tests are passing, on the Mac the coeff_signed_to_unsigned fails just like in CI.
I can't confirm that CI behaves differently than running locally.

Most obvious thing that is not controlled by nix on Mac is the compiler version, as we are using the native clang on Mac. Could it maybe be related to your issue? I'm more guessing than anything here.

I have this clang version on the Mac:

$ gcc --version
Apple clang version 15.0.0 (clang-1500.3.9.4)
Target: arm64-apple-darwin23.5.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

Can send more outputs if needed.

[rod-chapman]

That's interesteing. I have Apple M1 Pro running macOS 13.6.7 with

rodchap@f4d4889dcf6d ~ % gcc --version
Apple clang version 15.0.0 (clang-1500.1.0.2.5)
Target: arm64-apple-darwin22.6.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

and the proof of coeff_signed_to_unsigned() works every time, using both a native shell and running NIX.

I also tried again using a native build of gcc 13.1.0 on PATH before /usr/bin and that also works both with and without NIX.

Using Apple's clang 15 on PATH in /usr/bin/gcc, I just ran

goto-cc -E -DCBMC -I../../../fips202 -I../../../mlkem ../../../mlkem/poly.c

(using CBMC 6.0.0) and I got the attached file.
[
poly_clang_expanded.i.gz
](url)
What do you get on the Mac where the proof fails?

[mkannwischer]

output.txt

[rod-chapman]

Darn... different in comments only. So... what else could be different?

[rod-chapman]

I have an Intel-based Mac here running Sonoma 14.5 with same clang version as you report above.
Aha... it fails... "make -f desktop.mk" runs, but significantly...

cbmc --verbosity 6 --object-bits 8 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --smt2 ../../../mlkem/poly_contracts.goto
CBMC version 6.0.1 (cbmc-6.0.1) 64-bit x86_64 macos
Reading GOTO program from file ../../../mlkem/poly_contracts.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3

** Results:
../../../mlkem/poly.c function coeff_signed_to_unsigned
[coeff_signed_to_unsigned.no_alloc_dealloc_in_ensures.1] line 108 Check that ensures do not allocate or deallocate memory: SUCCESS
[coeff_signed_to_unsigned.no_alloc_dealloc_in_requires.1] line 108 Check that requires do not allocate or deallocate memory: SUCCESS
[coeff_signed_to_unsigned.no_recursive_call.1] line 108 No recursive call to function coeff_signed_to_unsigned when checking contract coeff_signed_to_unsigned: SUCCESS
[coeff_signed_to_unsigned.single_top_level_call.1] line 108 Only a single top-level call to function coeff_signed_to_unsigned when checking contract coeff_signed_to_unsigned: SUCCESS
[coeff_signed_to_unsigned.assigns.1] line 110 Check that r is assignable: SUCCESS
[coeff_signed_to_unsigned.assigns.2] line 113 Check that factor is assignable: SUCCESS
[coeff_signed_to_unsigned.assigns.3] line 114 Check that r is assignable: SUCCESS
[coeff_signed_to_unsigned.overflow.3] line 114 arithmetic overflow on signed * in factor * 3329: ERROR
[coeff_signed_to_unsigned.overflow.4] line 114 arithmetic overflow on signed + in r + factor * 3329: ERROR
[coeff_signed_to_unsigned.assertion.1] line 116 coeff_signed_to_unsigned result lower bound: ERROR
[coeff_signed_to_unsigned.assertion.2] line 117 coeff_signed_to_unsigned result upper bound: ERROR
[coeff_signed_to_unsigned.overflow.5] line 120 arithmetic overflow on signed to unsigned type conversion in (uint16_t)r: ERROR
[coeff_signed_to_unsigned.postcondition.1] file ../../../mlkem/poly.h line 53 Check ensures clause of contract contract::coeff_signed_to_unsigned for function coeff_signed_to_unsigned: ERROR
[coeff_signed_to_unsigned.postcondition.2] file ../../../mlkem/poly.h line 54 Check ensures clause of contract contract::coeff_signed_to_unsigned for function coeff_signed_to_unsigned: ERROR
[coeff_signed_to_unsigned.overflow.1] file ../../../mlkem/poly.h line 55 arithmetic overflow on signed * in (signed int)((int32_t)c_wrapper < 0) * 3329: ERROR
[coeff_signed_to_unsigned.overflow.2] file ../../../mlkem/poly.h line 55 arithmetic overflow on signed + in (int32_t)c_wrapper + (signed int)((int32_t)c_wrapper < 0) * 3329: ERROR
[coeff_signed_to_unsigned.postcondition.3] file ../../../mlkem/poly.h line 55 Check ensures clause of contract contract::coeff_signed_to_unsigned for function coeff_signed_to_unsigned: ERROR

[rod-chapman]

I feel very stupid.

For the "--smt2" option to work, you need "z3" on PATH, or it just silently says "ERROR". Can we add z3 to the NIX config?

[mkannwischer]

Yes, that should be easy. I can look into this.

[rod-chapman]

Thanks. I have already raised diffblue/cbmc#8362

[rod-chapman]

Z3 4.13.0 appears to be "latest". Can we settle on that for all our development platforms?

[mkannwischer]

I can't push to this branch, but if you apply the following patch, it should install 4.8.17

diff --git a/flake.nix b/flake.nix
index d0efeaa..bcce88a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -61,6 +61,7 @@
                 yq
                 ninja# 1.11.1
                 qemu# 8.2.4
+                z3# 4.8.17
                 cadical;

Can we try that first or do we need a specific version?
There is also z3_4_12 (4.12.5) that's prepackaged in the nix repo.
If you need anything newer, we have to compile from source.

[mkannwischer]

Btw, I confirmed that this solves the issue on my Mac.

[rod-chapman]

Let's go for a latest version that pre-packaged in NIX, so 4.12.5 then...

[rod-chapman]

Confirmed... adding "z3_4_12" in flake.nix gets me Z3 4.12.5. I will try to open a PR to add that.

[mkannwischer]

I've rebased this on top of main after #85 was merged adding the required z3 dependency.

@rod-chapman, apologies for guessing wrongly.
Indeed z3 was installed on my x86 machine while it wasn't on the Mac.
Glad to see it is now working and CI was indeed working as expected and helping us to catch such errors.

Is this PR now ready to be reviewed/merged?

[rod-chapman]

If the CI runners are all good now, then yes - please review.

[rod-chapman]

I just need to back out the debugging changes... hang on...

[rod-chapman]

OK... debugging options removed...

[rod-chapman]

Looks good. Please review.

[cothan]

I have one minor comments. Other than that, the PR LGTM.

[rod-chapman]

Good to merge?

[cothan]

Yep. I think it's good to merge.

[hanno-becker]

I'll review tomorrow morning.

[hanno-becker]

@rod-chapman We should strive for a clean history before merging PRs; that is, squash fixup commits into the commits they apply to, remove any test-commits that are later undone, etc. Since your PR has been waiting for so long, I took the liberty to do this myself, but generally it should be the PR author.

I have also renamed coeff_signed_to_unsigned to scalar_signed_to_unsigned_q_16, in line with other functions. I also added a TODO + WARNING regarding the sign-extractor expression r < 0 which is prone to introducing branches, I think.

[hanno-becker]

After further consultation with @mkannwischer, we don't think it's acceptable even temporarily to introduce the unprotected r < 0 expression. We should instead use / introduce a suitable primitive from verify.c. For example, we could use cmov_int16(&r, r + KYBER_Q, r < 0).

[rod-chapman]

Noted and understood. I will update my branch and take a look at verify.c