MicroPython + SPARK Ada Multicore Demo

This repository contains a full-fledged example of interfacing MicroPython running on the Raspberry Pi Pico 2 (RP2350) with a formally verified backend written in Ada SPARK.

It demonstrates a robust bare-metal architecture:

1. Scriptable Python Frontend (Core 0): Executes high-level asyncio tasks and application loops.
2. Formally Verified Backend (Core 1): Executes native ARM Cortex-M33 machine instructions compiled from SPARK Ada code, mathematically proven correct and free of runtime errors.

---

1. Project Structure

• main.py: Test script calling the SPARK module and catching boundary overflow exceptions.
• src/spark_core.ads & spark_core.adb: Core SPARK package containing mathematical functions with pre/post-condition contracts.
• src/micropython_ada.ads & src/micropython_ada.adb: Ada translation boundary. It extracts C integers from mp_obj_t values, checks preconditions, and executes verified logic.
• src/adamodule.c: C module registering the Ada entry points with MicroPython's runtime globals.
• src/micropython.cmake: CMake rules for compile, elaboration binding (gnatbind), and library packaging (libspark.a).

---

2. Compilation & Setup

To compile this project, you need the ARM Bare-Metal Ada/SPARK Toolchain (gnat-arm / arm-eabi-gcc).

1. Clone this repository as a sibling of the MicroPython repository.
2. Run the MicroPython compilation, pointing the USER_C_MODULES CMake argument to the CMake rules in this project:

cd /path/to/micropython/ports/rp2
make BOARD=RPI_PICO2 DEBUG=1 USER_C_MODULES=/path/to/micropython-spark-demo/src/micropython.cmake

This compiles MicroPython, compiles the Ada files, runs gnatbind to generate the package elaboration bindings, packs the results into libspark.a, and links everything together into firmware.elf.

---

3. Formal Verification with SPARK

Before building, you can mathematically prove that the SPARK code is free from runtime exceptions (such as integer overflows, division-by-zero, or boundary violations) by running the SPARK prover (gnatprove):

gnatprove -P spark_project.gpr

The Alt-Ergo/Z3 theorem provers will scan the preconditions and guarantee that the implementation body satisfies them under all possible inputs, proving the code structurally correct.

---

4. GDB Debugging Walkthrough

Once the target Pico 2 is flashed, launch a GDB debug session connecting to your SWD programmer (e.g. OpenOCD):

gdb-multiarch /path/to/micropython/ports/rp2/build-RPI_PICO2/firmware.elf
(gdb) target remote localhost:3333

A. Setting Breakpoints in Ada

You can set breakpoints directly on the Ada packages and functions:

(gdb) break SPARK_Core.Safe_Add
Breakpoint 1 at 0x1003c004: file spark_core.adb, line 5.

B. Language Inspection

When the breakpoint hits, check the execution context. GDB automatically changes its expression evaluator to Ada:

(gdb) show language
The current source language is "ada".

Print variables and evaluate their types:

(gdb) print A_Spark
$1 = 1234
(gdb) ptype A_Spark
type = range -1073741824 .. 1073741823

C. Viewing the Mixed Stack Trace

Type backtrace (or bt) to inspect a seamless, mixed C/Python/Ada/SPARK call stack:

#0  SPARK_Core.Safe_Add (A=1234, B=5678) at spark_core.adb:5
#1  0x1003be22 in MicroPython_Ada.Ada_Add_Ints (A_Obj=2469, B_Obj=11357) at micropython_ada.adb:20
#2  0x1003bfa8 in ada_add_ints (a_obj=2469, b_obj=11357) at adamodule.c:5
#3  0x1001497a in fun_builtin_1_call (self_in=..., args=...) at py/objfun.c:70
#4  0x20003392 in mp_execute_bytecode (code_state=...) at py/vm.c:1069

This stack trace displays the exact sequence:

1. MicroPython bytecode execution loop (mp_execute_bytecode in C).
2. Python-to-C wrapper dispatch (fun_builtin_1_call).
3. C glue layer registering our exports (ada_add_ints in C).
4. Ada boundary parsing the arguments (Ada_Add_Ints in Ada).
5. Verified SPARK math logic (Safe_Add in SPARK).