Add Renode emulation tests for Cortex-M4F and Cortex-M33

.github/workflows/renode-tests.yml

@@ -1,10 +1,13 @@
-# Multi-architecture build verification
+# Renode emulation tests for Gale on M4F and M33 architectures
 #
-# Builds Zephyr+Gale semaphore test for M4F, M33, and R5 targets.
-# Proves the Rust FFI cross-compiles correctly for each architecture.
-# Renode emulation tests will be added once renode-bazel-rules is wired in.
+# Builds Zephyr+Gale semaphore test for each board with west, then runs
+# the Renode Robot Framework tests to verify correct execution on the
+# emulated hardware.  Complements zephyr-tests.yml (which uses QEMU M3)
+# by covering hardware-accurate M4F (STM32F4) and M33 (STM32L552/nucleo_l552ze_q) emulation.
+#
+# Renode portable handles its own .NET runtime — no system deps needed.
 
-name: Multi-Arch Build
+name: Renode Emulation Tests
 
 on:
   push:
@@ -17,28 +20,28 @@ env:
   DOCKER_CONFIG: /tmp/.docker
 
 jobs:
-  build:
+  renode-test:
     name: "${{ matrix.arch }} (${{ matrix.board }})"
     runs-on: ubuntu-22.04
+    timeout-minutes: 30
     container:
       image: ghcr.io/zephyrproject-rtos/ci:v0.29.0
       options: --user root
     strategy:
       fail-fast: false
       matrix:
         include:
-          - board: mps2/an385
-            arch: cortex-m3
-            rust_target: thumbv7m-none-eabi
-            test_path: tests/kernel/semaphore/semaphore
-          - board: mps2/an386
-            arch: cortex-m4
+          - board: stm32f4_disco
+            arch: cortex-m4f
             rust_target: thumbv7em-none-eabihf
             test_path: tests/kernel/semaphore/semaphore
-          - board: mps2/an521/cpu0
+            robot_file: stm32f4_sem.robot
+
+          - board: nucleo_l552ze_q
             arch: cortex-m33
             rust_target: thumbv8m.main-none-eabihf
             test_path: tests/kernel/semaphore/semaphore
+            robot_file: stm32l552_sem.robot
 
     steps:
       - name: Checkout Gale
@@ -54,7 +57,7 @@ jobs:
           curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable
           . /root/.cargo/env
           rustup target add "${RUST_TARGET}"
-          # Also install non-hf variant in case FPU is disabled
+          # Install non-hf variant in case the board uses soft-float ABI
           NON_HF=$(echo "${RUST_TARGET}" | sed 's/eabihf$/eabi/')
           if [ "${NON_HF}" != "${RUST_TARGET}" ]; then
             rustup target add "${NON_HF}" || true
@@ -68,7 +71,7 @@ jobs:
           west update --narrow -o=--depth=1
           west sdk install
 
-      - name: Build semaphore test
+      - name: Build Zephyr+Gale ELF
         env:
           BOARD: ${{ matrix.board }}
           TEST_PATH: ${{ matrix.test_path }}
@@ -83,6 +86,30 @@ jobs:
             -DZEPHYR_EXTRA_MODULES="${GALE_ROOT}" \
             -DOVERLAY_CONFIG="${GALE_ROOT}/zephyr/gale_overlay.conf"
 
+      - name: Install Robot Framework
+        run: |
+          # The Zephyr CI Docker image (ci:v0.29.0) includes Renode pre-installed
+          # at /opt/renode (already in PATH). Just install Robot Framework.
+          pip3 install robotframework
+
+      - name: Run Renode test
+        env:
+          ROBOT_FILE: ${{ matrix.robot_file }}
+          ELF: ${{ github.workspace }}/zephyr-workspace/build/zephyr/zephyr.elf
+        run: |
+          GALE_ROOT="${GITHUB_WORKSPACE}/gale"
+          mkdir -p "${GITHUB_WORKSPACE}/renode-results"
+          cd "${GITHUB_WORKSPACE}/renode-results"
+          renode-test "${GALE_ROOT}/renode/${ROBOT_FILE}"
+
+      - name: Upload Renode results
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: "renode-results-${{ matrix.arch }}"
+          path: renode-results/
+          retention-days: 7
+
       - name: Upload ELF
         if: success()
         uses: actions/upload-artifact@v4

Cargo.toml

@@ -46,7 +46,7 @@ overflow-checks = true
 # Core safety lints
 unsafe_code = "deny"
 # TODO: enable missing_docs = "warn" once all items are documented
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(verus_keep_ghost)'] }
 
 [lints.clippy]
 # === DENY: Correctness & safety-critical ===

README.md

@@ -116,8 +116,8 @@ Triple-track formal verification:
 | Workflow | Scope | Status |
 |----------|-------|--------|
 | Rust CI | cargo test, clippy, verus-strip gate | 995 tests |
-| Zephyr Kernel Tests | 13 upstream test suites on qemu_cortex_m3 | 13/13 pass |
-| Multi-Arch Build | M3, M4F, M33 cross-compilation | 3 boards |
+| Zephyr Kernel Tests | 20 upstream test suites on qemu_cortex_m3 | 20/20 pass |
+| Renode Emulation Tests | Cortex-M4F (STM32F4) + Cortex-M33 (STM32L552) | 2 boards |
 
 ## Traceability
 

artifacts/design.yaml

@@ -3604,3 +3604,89 @@ artifacts:
         target: SWREQ-SM-SM02
       - type: function-maps-to
         target: PROV-SM-001
+
+  # ── Integration test targets (SWE.5 / SWE.6) ─────────────────────────
+  #
+  # These architecture decisions capture the hardware/emulation platforms
+  # used for Zephyr integration and Renode emulation testing.
+  # Kiln and Synth can reference these IDs to declare compatibility or
+  # to specify which targets their code generation must pass on.
+
+  - id: SWARCH-TGT-001
+    type: sw-arch-component
+    title: Integration test target — QEMU Cortex-M3 (qemu_cortex_m3)
+    status: approved
+    description: >
+      Primary Zephyr integration test target for Gale kernel primitives.
+      20 upstream Zephyr test suites (semaphore, mutex, condvar, msgq,
+      stack, pipe, timer, event, sched, thread, and more) run on the
+      qemu_cortex_m3 board under west + QEMU.  All 20/20 suites pass
+      with Gale replacing the corresponding C kernel modules.
+      Chosen for QEMU Cortex-M3 availability in Zephyr CI Docker image
+      without hardware setup — the canonical CI board for Zephyr kernel tests.
+    tags: [test-target, qemu, cortex-m3, integration]
+    fields:
+      platform: qemu_cortex_m3
+      emulator: QEMU (via west build -t run)
+      architecture: ARMv7-M (Cortex-M3, no FPU)
+      rust-target: thumbv7m-none-eabi
+      ci-workflow: .github/workflows/zephyr-tests.yml
+      test-suites: 20
+    links:
+      - type: allocated-from
+        target: SYSREQ-SEM-001
+
+  - id: SWARCH-TGT-002
+    type: sw-arch-component
+    title: Renode emulation target — STM32F4 Discovery (Cortex-M4F)
+    status: approved
+    description: >
+      Hardware-accurate Renode emulation target for Cortex-M4F (ARMv7E-M
+      with FPU) validation.  The stm32f4_disco board with stm32f4_discovery.repl
+      platform runs Gale semaphore tests under Renode 1.16.0 (pre-installed
+      in Zephyr CI Docker image).  Confirms Gale functions correctly on
+      hardware with hardware floating-point and higher clock rates than M3.
+      Chosen because stm32f4_discovery.repl is fully emulated in Renode 1.16.0
+      with working USART2 for Zephyr console output.
+    tags: [test-target, renode, cortex-m4f, stm32f4]
+    fields:
+      platform: stm32f4_disco
+      emulator: Renode 1.16.0 (renode-test via Robot Framework)
+      renode-platform: platforms/boards/stm32f4_discovery.repl
+      architecture: ARMv7E-M (Cortex-M4F, with FPU)
+      rust-target: thumbv7em-none-eabihf
+      ci-workflow: .github/workflows/renode-tests.yml
+      uart: sysbus.usart2
+    links:
+      - type: allocated-from
+        target: SYSREQ-SEM-001
+      - type: enables
+        target: SWREQ-KILN-003
+
+  - id: SWARCH-TGT-003
+    type: sw-arch-component
+    title: Renode emulation target — STM32L552 Nucleo (Cortex-M33)
+    status: approved
+    description: >
+      Hardware-accurate Renode emulation target for Cortex-M33 (ARMv8-M
+      Mainline with TrustZone) validation.  The nucleo_l552ze_q board with
+      the Renode nucleo_l552ze_q_ns platform runs Gale semaphore tests
+      under Renode 1.16.0.  Confirms Gale functions on ARMv8-M which
+      introduces security extension changes to the exception model.
+      Chosen because Renode 1.16.0 ships a dedicated test platform
+      (tests/platforms/nucleo_l552ze_q/nucleo_l552ze_q_ns.repl) with
+      complete STM32L552 peripheral support including LPUART1.
+    tags: [test-target, renode, cortex-m33, stm32l552]
+    fields:
+      platform: nucleo_l552ze_q
+      emulator: Renode 1.16.0 (renode-test via Robot Framework)
+      renode-platform: tests/platforms/nucleo_l552ze_q/nucleo_l552ze_q_ns.repl
+      architecture: ARMv8-M Mainline (Cortex-M33, with FPU + TrustZone)
+      rust-target: thumbv8m.main-none-eabihf
+      ci-workflow: .github/workflows/renode-tests.yml
+      uart: sysbus.lpuart1
+    links:
+      - type: allocated-from
+        target: SYSREQ-SEM-001
+      - type: enables
+        target: SWREQ-KILN-003

artifacts/phase2_kiln_integration.yaml

@@ -147,6 +147,10 @@ artifacts:
     links:
       - type: derives-from
         target: SYSREQ-KILN-002
+      - type: verified-on
+        target: SWARCH-TGT-002
+      - type: verified-on
+        target: SWARCH-TGT-003
 
   - id: SWREQ-KILN-004
     type: sw-req

plain/src/event.rs

@@ -58,7 +58,9 @@ impl Event {
     ///
     /// Returns the resulting event bitmask.
     pub fn post(&mut self, new_events: u32) -> u32 {
+        let old_events = self.events;
         self.events = self.events | new_events;
+        let new_val = self.events;
         self.events
     }
     /// Set the event bitmask to an exact value, replacing all bits.

plain/src/fatal.rs

@@ -76,7 +76,11 @@ pub struct FatalError {
 }
 impl FatalError {
     /// Create a fatal error event.
-    pub fn new(reason: FatalReason, context: FatalContext, test_mode: bool) -> FatalError {
+    pub fn new(
+        reason: FatalReason,
+        context: FatalContext,
+        test_mode: bool,
+    ) -> FatalError {
         FatalError {
             reason,
             context,
@@ -93,29 +97,37 @@ impl FatalError {
         if !self.test_mode {
             match self.reason {
                 FatalReason::KernelPanic => RecoveryAction::Halt,
-                FatalReason::CpuException => match self.context {
-                    FatalContext::Isr => RecoveryAction::Halt,
-                    FatalContext::Thread => RecoveryAction::AbortThread,
-                },
-                FatalReason::SpuriousIrq => match self.context {
-                    FatalContext::Isr => RecoveryAction::Halt,
-                    FatalContext::Thread => RecoveryAction::AbortThread,
-                },
+                FatalReason::CpuException => {
+                    match self.context {
+                        FatalContext::Isr => RecoveryAction::Halt,
+                        FatalContext::Thread => RecoveryAction::AbortThread,
+                    }
+                }
+                FatalReason::SpuriousIrq => {
+                    match self.context {
+                        FatalContext::Isr => RecoveryAction::Halt,
+                        FatalContext::Thread => RecoveryAction::AbortThread,
+                    }
+                }
                 FatalReason::StackCheckFail => RecoveryAction::AbortThread,
-                FatalReason::KernelOops => match self.context {
-                    FatalContext::Isr => RecoveryAction::Halt,
-                    FatalContext::Thread => RecoveryAction::AbortThread,
-                },
+                FatalReason::KernelOops => {
+                    match self.context {
+                        FatalContext::Isr => RecoveryAction::Halt,
+                        FatalContext::Thread => RecoveryAction::AbortThread,
+                    }
+                }
             }
         } else {
             match self.context {
-                FatalContext::Isr => match self.reason {
-                    FatalReason::SpuriousIrq => RecoveryAction::Ignore,
-                    FatalReason::StackCheckFail => RecoveryAction::AbortThread,
-                    FatalReason::CpuException => RecoveryAction::Ignore,
-                    FatalReason::KernelOops => RecoveryAction::Ignore,
-                    FatalReason::KernelPanic => RecoveryAction::Ignore,
-                },
+                FatalContext::Isr => {
+                    match self.reason {
+                        FatalReason::SpuriousIrq => RecoveryAction::Ignore,
+                        FatalReason::StackCheckFail => RecoveryAction::AbortThread,
+                        FatalReason::CpuException => RecoveryAction::Ignore,
+                        FatalReason::KernelOops => RecoveryAction::Ignore,
+                        FatalReason::KernelPanic => RecoveryAction::Ignore,
+                    }
+                }
                 FatalContext::Thread => RecoveryAction::AbortThread,
             }
         }