Step 53 of 56

Testing and proof: reproducing the claims

Thirty-two harnesses run on your PC, not the board. Half check behaviour against the host's own tools; half prove absence of run-time errors outright.

Why so much runs on the host

Most of what this SDK does is pure logic over a thin hardware seam — a filesystem over Block_Dev, a DNS message builder over GNAT.Sockets, a clock-divider calculation. Logic like that is target-independent, so it can be exercised on a PC in a second rather than flashed and watched over a serial cable.

That split is deliberate and it tells you where a bug lives. The ext4_host harness builds the same filesystem sources the firmware uses — its project's Source_Files whitelist pulls in every portable unit and omits only the on-target block adapters. So a bug that reproduces on the host is a real filesystem bug, and one that appears only on target points at the SD/SPI layer instead.

Running a host test

Each harness under libs/esp32s3_hal/test/ carries its own run.sh, which finds the Alire native toolchain itself:

bash libs/esp32s3_hal/test/endian_host/run.sh
bash libs/esp32s3_hal/test/ext4_host/run.sh

The first is instant and self-contained:

ESP32S3.Endian equivalence check:
  little-endian join/split . PASS ( 4096 cases)
  big-endian 32 join/split . PASS ( 4096 cases)
  big-endian 16 join/split . PASS ( 65536 cases)

The second needs e2fsprogs, because it does something better than checking its own answers — it cross-checks every volume against the Linux kernel's own e2fsck:

  dirgrow        e2fsck CLEAN
      dirgrow: 400 files + 101 replaced, missing 0
  stream         e2fsck CLEAN
      stream: 205500 bytes via Append, readback OK

The same pattern recurs: fat16_host makes three independent implementations agree (this code, dosfstools, and a writer written from the specification), modbus_*_host talk to a standard client, and esp_loader_host drives a simulated ROM that validates every frame and impersonates each chip family in turn.

Proof, not just testing

A test shows the cases you thought of pass. SPARK proves a property holds for every input. The proof projects run at --level=1 — "silver": no overflow, no array index out of range, no division by zero, and all loops terminate.

cd libs/esp32s3_hal/test/ledc_math_prove
gnatprove -P ledc_math_prove.gpr --level=1 --report=statistics

Which reports, per check, what was proved and by which solver:

esp32s3-ledc-math.adb:27:18: info: division check proved (Z3)
esp32s3-ledc-math.ads:17:13: info: implicit aspect Always_Terminates on
                                   "Clock_Divider" has been proved
esp32s3-ledc-math.ads:19:19: info: postcondition proved (Z3)
esp32s3-ledc-math.ads:26:19: info: postcondition proved (altergo)

Note the last two: these are not only absence of run-time errors but postconditions — the divider really does produce a frequency within tolerance, for every input, not merely for the values someone tried.

How a unit joins the proof surface

A unit is proven by carrying with SPARK_Mode => On on its spec and body; I/O, access types and raising operations at the boundary get SPARK_Mode => Off, and GNATprove analyses the On subset automatically.

That is why the proven parts are the shapes they are — parsers, serialisers, checksums, routing and date arithmetic, clock-divider maths. The *_math children exist precisely so the arithmetic can be separated from the register writes and proven on its own: LEDC.Math, MCPWM.Math, RMT.Math, TWAI.Math, Ext4.Mkfs.Math. The driver body that writes registers stays unmarked.

Proof at silver level says the code cannot fail at run time and meets its stated contracts. It does not say the contract is the one you wanted, nor that the hardware behaves as the datasheet claims. It complements the hardware self-tests in the examples; it does not replace them.

book/prove/prove.sh runs the proof across every unit marked for it, if you want the whole surface rather than one project.