Cross-platform instability arising from default signedness of char in contracts library

[rod-chapman]

In GOTO arising from the mlkem-native codebase, we're still seeing some cross-platform differences (i.e. between macOS and Linux) regarding casts to/from "char *" where the default signedness of "char" is implementation-defined, using CBMC 6.9.0

A small isolated example: the function scalar_signed_to_unsigned_q() in mlkem/src/poly.c, the GOTO generated by goto-instrument on Mac vs Linux contains the following single difference:

$ diff mac2/f.txt lnx2/f.txt 
140c140
<         ASSIGN __CPROVER_contracts_write_set_check_assignment::1::ub := cast(cast(__CPROVER_contracts_write_set_check_assignment::ptr, signedbv[8]*) + cast(__CPROVER_contracts_write_set_check_assignment::size, signedbv[64]), empty*)
---
>         ASSIGN __CPROVER_contracts_write_set_check_assignment::1::ub := cast(cast(__CPROVER_contracts_write_set_check_assignment::ptr, unsignedbv[8]*) + cast(__CPROVER_contracts_write_set_check_assignment::size, signedbv[64]), empty*)

This difference knocks-on to cause instability in the generated SMT, and unstable behaviour of Z3.

I think the solution is still to fix the signedness of "char" in a few places in cprover_contract.c, such as

cbmc/src/ansi-c/library/cprover_contracts.c

Line 141 in a6531d4

.is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};

To be confirmed.

[tautschnig]

In GOTO arising from the mlkem-native codebase, we're still seeing some cross-platform differences (i.e. between macOS and Linux) regarding casts to/from "char *" where the default signedness of "char" is implementation-defined, using CBMC 6.9.0

That difference at the GOTO-program level is expected, and when previously studying this we found the formulae to be the same (after applying #8836 (and also #8830)).

Can you point me to the exact mlkem-native proof where you are seeing Z3 to have unstable behaviour? I'd like to reconfirm that we genuinely produce different formulae across the different platforms.

[rod-chapman]

Indeed - I thought that #8836 had fixed this, but the difference is still there.

[rod-chapman]

The biggest/slowest/most-unstable proof in mlkem-native is the function mlk_indcpa_keypair_derand() in mlkem/src/indcpa.c

BUT... that function is really big, and it's hard to see the wood for the trees in the GOTO and SMT that it generates. If you want a simple, isolated example of this particular issue, then look at scalar_signed_to_unsigned_q() in mlkem/src/poly.c, which is the smallest, simplest function that I could find that shows this problem.

[rod-chapman]

A quick experiment confirms that changing (char *) to (unsigned char *) (7 times) in src/ansi-c/library/cprover_contracts.c yields identical results (i.e. unsignedbv[8]) on both macOS and Linux for this small example.

[tautschnig]

A quick experiment confirms that changing (char *) to (unsigned char *) (7 times) in src/ansi-c/library/cprover_contracts.c yields identical results (i.e. unsignedbv[8]) on both macOS and Linux for this small example.

When you said "identical results" - is that in terms of solver time or just the GOTO functions?

[rod-chapman]

Identical output from ‘goto-instrument —show-goto-functions’ and identical SMT output

[tautschnig]

Thanks for confirming. One important data point from my own experiments (x86_64 Linux, simulating the platform difference via -funsigned-char, using the scalar_signed_to_unsigned_q proof pipeline): the SMT2 output (--smt2 --z3 --outfile) is byte-identical across the two char-signedness configurations even without any patch — on CBMC 6.8, 6.9, and current develop — and so is --dimacs output. Pointer-to-pointer casts are width-preserving no-ops in the bit-level encoding, so the char * vs unsigned char * difference in the GOTO text never reaches the formula. That means #9081 is a worthwhile GOTO-text stability fix, but the SMT for this scenario was already stable, and the "unstable behaviour of Z3" reported here must have a different cause — differing Z3 builds between macOS and Linux would be my first suspect. If you have a pair of diverging .smt2 files produced by the same CBMC version on the two platforms, I'd very much like to see them.

The investigation did turn up one genuine char-signedness-dependent SMT instability, but in the incremental SMT back-end only (not used by mlkem-native's Makefiles): the emission order of size_of_object/is_dynamic_object assertions follows expression-hash order. A fix (emitting them in deterministic object-id order) is ready and I'll put it up as a PR shortly.

[tautschnig]

Follow-up with data from an aarch64 host: I re-ran the full sign_verify_internal pipeline twice on identical hardware/OS with only the char-signedness ABI toggled (native unsigned vs -fsigned-char, i.e. the Linux/macOS difference). The GOTO text shows the familiar 13 char * cast differences — but the generated SMT2 (~550k lines) is byte-identical. Meanwhile, the actual macOS-vs-Linux .smt2 pairs for this proof differ structurally (20316 vs 20310 assertions, differing branch guards, extra call-argument symbols on Linux, first divergence near the __CPROVER_contracts_is_fresh expansion): the two platforms are verifying slightly different programs. Those differences cannot stem from char signedness (or the controlled experiment would show them) and will persist after #9081. Likely candidates are system-header differences (e.g. fortify __*_chk wrappers) or OS-conditional library models. @rod-chapman could you share --show-goto-functions dumps from mac and Linux for one of these proofs so we can pin down the true source of the formula divergence?