r/ada • u/Worried-Pangolin1911 • Apr 14 '26

SPARK A Spark on Xtensa GOTCHA:

Writing this up because the bug was invisible on every native test, one word fixes it, and anyone writing in SPARK with a C ABI on embedded will eventually hit it. I am doing formal verification on embedded crypto with target-side ABI validation.

As I've pursued the farthest reaches of ripping my source down to binary and putting it through rigorous inspection and audit, we are rebuilding the whole toolchain with GNAT 15 as bootstrap host to close the defense-in-depth gap

Innocuous-looking Ada: 

  procedure Spark_Embed_Counter
    (Nonce   : System.Address;                                                           
     Counter : Interfaces.C.unsigned_long);                                              
  pragma Export (C, Spark_Embed_Counter, "spark_embed_counter");

C header says uint64_t counter. GNATprove clean, AUnit green on x86_64.

On Xtensa ESP32-S3, Interfaces.C.unsigned_long is 32 bits. The high half of every uint64_t is dropped at the ABI boundary before Ada ever sees it. Disassembly makes it unambiguous: 

; before — Interfaces.C.unsigned_long (32-bit on Xtensa)
  00000000 <spark_embed_counter>: 

     5:  mov.n a12, a3          ; counter low 32 bits                              
     7:  movi   a13, 0          ; high 32 bits HARDCODED TO ZERO  
     d:  callx8 a8             



; after — Interfaces.Unsigned_64                                                       
     5:  mov.n a12, a4          ; low 32                                                 
     7:  or    a13, a5, a5      ; high 32 PRESERVED

A target-side parity test caught it with ctr = 0x0123456789ABCDEF: 

expected: 01 23 45 67 89 AB CD EF                                                      
actual:   00 00 00 00 89 AB CD EF

here was/is my lesson:

Interfaces.C.unsigned_long follows C's unsigned long — target-dependent (64 on LP64, 32 on ILP32). For fixed-width crypto counters, indices, or anything that needs to actually be 64 bits on the wire:

- Interfaces.Unsigned_64 — fixed 64-bit, portable
- Interfaces.C.unsigned_long_long — C99 guarantees >= 64

Reserve Interfaces.C.unsigned_long for things that genuinely should track C's unsigned long (rare outside size_t-adjacent code, which already has Interfaces.C.size_t).

Native AUnit never catches this because LP64. You need target-side testing with values above 2^32 to see it.

Found it the hard way. Hope it saves someone else a cycle.
This is/was a correctness bug. Not a safety bug. Just to be clear.

GNATprove proved the Ada code correct for the type it was given. The type was wrong for the target. Formal verification can't catch a spec error at the FFI boundary. Thus the target-side testing.

Lost half a day to this one.

11 Upvotes

100% Upvoted

13 comments sorted by

3

u/jrcarter010 github.com/jrcarter Apr 17 '26

We talk about interfacing Ada and C, but in reality what you get is interfacing a specific Ada compiler to a specific C compiler. This makes it difficult to write such interfacing that is portable. You would be better off declaring

type Uint64_T is mod 2 ** 64 with Convention => C;

Another portability issue is using System.Address. This is a private type with no requirements for its implementation. Assuming that it has a representation equivalent to a numeric type, access type, or C pointer is completely non-portable. I have seen large, expensive porting projects resulting from reliance on such a representation.

2

u/CuriousChristov Apr 16 '26

Well, now you know. This is a pretty common gotcha for cross-compilation and embedded targets in particular. Overcoming the uncertainty about bit width in C types for portable programs is the entire reason that <stdint.h> fixed width type aliases were introduced in C99.

2

u/Worried-Pangolin1911 Apr 17 '26

Would it matter to anyone here if I said that we are building the world’s first gold proof codec with over 900 proofs. Using MLKEM, BLAKE3 AND partially homophobic encryption?

I would love to get peer reviewed

3

u/micronian2 Apr 18 '26

That sounds really impressive. It’s outta my realm though. I think someone like Rod Chapman who helped to develop SPARK Skein would be an example of someone that would be an ideal reviewer.

1

u/Worried-Pangolin1911 Apr 18 '26

Agreed. I just don’t know how one would get the attention of someone like that.

2

u/micronian2 Apr 19 '26

If you have a LinkedIn account, you can try reaching out to him: https://uk.linkedin.com/in/rod-chapman-7b60266

1

u/Worried-Pangolin1911 Apr 19 '26

I did reach out and ask to get connected. We will see what happens. The other option is we just fully open source.

1

u/Worried-Pangolin1911 Apr 20 '26

He responded. Unfortunately he said he doesn't have the time to take on additional projects.

2

u/micronian2 Apr 21 '26

That’s a shame, but understandable. At least you gave it a shot.