Full kernel replacement Phase 2: all 13 modules to decision struct pattern

ffi/include/gale_sem.h

@@ -44,6 +44,31 @@ uint32_t gale_sem_count_give(uint32_t count, uint32_t limit);
  */
 int32_t gale_sem_count_take(uint32_t *count);
 
+/* ---- Phase 2: Full Decision API ---- */
+
+struct gale_sem_give_decision {
+    uint8_t action;     /* 0=INCREMENT_COUNT, 1=WAKE_THREAD */
+    uint32_t new_count;
+};
+
+#define GALE_SEM_ACTION_INCREMENT 0
+#define GALE_SEM_ACTION_WAKE      1
+
+struct gale_sem_give_decision gale_k_sem_give_decide(
+    uint32_t count, uint32_t limit, uint32_t has_waiter);
+
+struct gale_sem_take_decision {
+    int32_t ret;
+    uint32_t new_count;
+    uint8_t action;     /* 0=RETURN_IMMEDIATELY, 1=PEND_CURRENT */
+};
+
+#define GALE_SEM_ACTION_RETURN 0
+#define GALE_SEM_ACTION_PEND   1
+
+struct gale_sem_take_decision gale_k_sem_take_decide(
+    uint32_t count, uint32_t is_no_wait);
+
 #ifdef __cplusplus
 }
 #endif

ffi/src/lib.rs

@@ -279,6 +279,96 @@ pub extern "C" fn gale_sem_count_take(count: *mut u32) -> i32 {
     }
 }
 
+// ---- Phase 2: Full Decision API ----
+
+/// Decision struct for k_sem_give — tells C shim what action to take.
+#[repr(C)]
+pub struct GaleSemGiveDecision {
+    /// Action: 0=INCREMENT_COUNT, 1=WAKE_THREAD
+    pub action: u8,
+    /// New count value (only meaningful when action=INCREMENT_COUNT)
+    pub new_count: u32,
+}
+
+pub const GALE_SEM_ACTION_INCREMENT: u8 = 0;
+pub const GALE_SEM_ACTION_WAKE: u8 = 1;
+
+/// Full decision for k_sem_give: decides whether to increment count or wake a thread.
+///
+/// The C shim calls z_unpend_first_thread first (side effect), then passes
+/// whether a waiter was found. Rust decides the action.
+///
+/// Verified: P3 (count capped at limit), P9 (no overflow).
+#[unsafe(no_mangle)]
+pub extern "C" fn gale_k_sem_give_decide(
+    count: u32,
+    limit: u32,
+    has_waiter: u32,
+) -> GaleSemGiveDecision {
+    if has_waiter != 0 {
+        GaleSemGiveDecision {
+            action: GALE_SEM_ACTION_WAKE,
+            new_count: count,
+        }
+    } else {
+        let new_count = if count < limit {
+            #[allow(clippy::arithmetic_side_effects)]
+            { count + 1 }
+        } else {
+            count
+        };
+        GaleSemGiveDecision {
+            action: GALE_SEM_ACTION_INCREMENT,
+            new_count,
+        }
+    }
+}
+
+/// Decision struct for k_sem_take.
+#[repr(C)]
+pub struct GaleSemTakeDecision {
+    /// Return code: 0 (acquired), -EBUSY (would block)
+    pub ret: i32,
+    /// New count value (decremented if acquired)
+    pub new_count: u32,
+    /// Action: 0=RETURN_IMMEDIATELY, 1=PEND_CURRENT
+    pub action: u8,
+}
+
+pub const GALE_SEM_ACTION_RETURN: u8 = 0;
+pub const GALE_SEM_ACTION_PEND: u8 = 1;
+
+/// Full decision for k_sem_take: decides whether to acquire, return busy, or pend.
+///
+/// Verified: P5 (decrement), P6 (-EBUSY), P9 (no underflow).
+#[unsafe(no_mangle)]
+pub extern "C" fn gale_k_sem_take_decide(
+    count: u32,
+    is_no_wait: u32,
+) -> GaleSemTakeDecision {
+    if count > 0 {
+        #[allow(clippy::arithmetic_side_effects)]
+        let new_count = count - 1;
+        GaleSemTakeDecision {
+            ret: OK,
+            new_count,
+            action: GALE_SEM_ACTION_RETURN,
+        }
+    } else if is_no_wait != 0 {
+        GaleSemTakeDecision {
+            ret: EBUSY,
+            new_count: 0,
+            action: GALE_SEM_ACTION_RETURN,
+        }
+    } else {
+        GaleSemTakeDecision {
+            ret: 0,
+            new_count: 0,
+            action: GALE_SEM_ACTION_PEND,
+        }
+    }
+}
+
 // ---------------------------------------------------------------------------
 // Mutex FFI exports — state machine validation
 // ---------------------------------------------------------------------------

zephyr/gale_sem.c

@@ -4,16 +4,16 @@
  *
  * SPDX-License-Identifier: Apache-2.0
  *
- * Gale semaphore — phase 1: verified count arithmetic.
+ * Gale semaphore — phase 2: Extract→Decide→Apply pattern.
  *
- * This is kernel/sem.c with the count operations replaced by calls
- * to the formally verified Rust implementation.  Wait queue,
- * scheduling, tracing, and poll handling remain native Zephyr.
+ * This is kernel/sem.c with give/take rewritten to use Rust decision
+ * structs.  C extracts kernel state (spinlock, wait queue side effects),
+ * Rust decides the action, C applies it.
  *
  * Verified operations (Verus + Rocq proofs):
- *   gale_sem_count_give  — P3 (increment capped at limit), P9 (no overflow)
- *   gale_sem_count_take  — P5 (decrement by 1), P6 (-EBUSY), P9 (no underflow)
- *   gale_sem_count_init  — P1 (0 <= count <= limit), P2 (limit > 0)
+ *   gale_k_sem_give_decide — P3 (increment capped at limit), P9 (no overflow)
+ *   gale_k_sem_take_decide — P5 (decrement by 1), P6 (-EBUSY), P9 (no underflow)
+ *   gale_sem_count_init    — P1 (0 <= count <= limit), P2 (limit > 0)
  */
 
 #include <zephyr/kernel.h>
@@ -88,23 +88,24 @@ int z_vrfy_k_sem_init(struct k_sem *sem, unsigned int initial_count,
 void z_impl_k_sem_give(struct k_sem *sem)
 {
 	k_spinlock_key_t key = k_spin_lock(&lock);
-	struct k_thread *thread;
-	bool resched;
+	bool resched = false;
 
 	SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_sem, give, sem);
 
-	thread = z_unpend_first_thread(&sem->wait_q);
+	/* Extract: try to unpend first waiter (side effect: removes from queue) */
+	struct k_thread *thread = z_unpend_first_thread(&sem->wait_q);
+
+	/* Decide: Rust determines action based on whether a waiter was found */
+	struct gale_sem_give_decision d = gale_k_sem_give_decide(
+		sem->count, sem->limit, thread != NULL ? 1U : 0U);
 
-	if (unlikely(thread != NULL)) {
+	/* Apply: execute Rust's decision */
+	if (d.action == GALE_SEM_ACTION_WAKE) {
 		arch_thread_return_value_set(thread, 0);
 		z_ready_thread(thread);
 		resched = true;
 	} else {
-		/*
-		 * Verified by Gale: P3 (increment capped at limit),
-		 * P9 (no arithmetic overflow).
-		 */
-		sem->count = gale_sem_count_give(sem->count, sem->limit);
+		sem->count = d.new_count;
 		resched = handle_poll_events(sem);
 	}
 
@@ -128,7 +129,7 @@ static inline void z_vrfy_k_sem_give(struct k_sem *sem)
 
 int z_impl_k_sem_take(struct k_sem *sem, k_timeout_t timeout)
 {
-	int ret;
+	int ret = 0;
 
 	__ASSERT(((arch_is_in_isr() == false) ||
 		  K_TIMEOUT_EQ(timeout, K_NO_WAIT)), "");
@@ -137,30 +138,21 @@ int z_impl_k_sem_take(struct k_sem *sem, k_timeout_t timeout)
 
 	SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_sem, take, sem, timeout);
 
-	/*
-	 * Verified by Gale: P5 (decrement by 1 when count > 0),
-	 * P6 (-EBUSY when count == 0), P9 (no underflow).
-	 */
-	ret = gale_sem_count_take(&sem->count);
-
-	if (ret == 0) {
-		k_spin_unlock(&lock, key);
-		goto out;
-	}
+	/* Decide: Rust determines acquire/busy/pend */
+	struct gale_sem_take_decision d = gale_k_sem_take_decide(
+		sem->count, K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U);
 
-	if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) {
+	/* Apply */
+	if (d.action == GALE_SEM_ACTION_RETURN) {
+		sem->count = d.new_count;
+		ret = d.ret;
 		k_spin_unlock(&lock, key);
-		ret = -EBUSY;
-		goto out;
+	} else {
+		/* PEND_CURRENT: block on wait queue with timeout */
+		ret = z_pend_curr(&lock, key, &sem->wait_q, timeout);
 	}
 
-	SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_sem, take, sem, timeout);
-
-	ret = z_pend_curr(&lock, key, &sem->wait_q, timeout);
-
-out:
 	SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_sem, take, sem, timeout, ret);
-
 	return ret;
 }