axonos-kernel v0.1.8

Author: AxonOS-BCI

Cargo.toml

@@ -18,7 +18,7 @@ exclude = [
 ]
 
 [workspace.package]
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"

axonos-capability/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-capability"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"

axonos-firmware-stm32f407/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-firmware-stm32f407"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
@@ -23,12 +23,12 @@ cortex-m-rt = "0.7"
 panic-halt = "0.2"
 
 # AxonOS workspace dependencies
-axonos-kernel-core = { version = "0.1.7", path = "../axonos-kernel-core" }
-axonos-time = { version = "0.1.7", path = "../axonos-time" }
-axonos-scheduler = { version = "0.1.7", path = "../axonos-scheduler" }
-axonos-capability = { version = "0.1.7", path = "../axonos-capability" }
-axonos-intent = { version = "0.1.7", path = "../axonos-intent" }
-axonos-spsc = { version = "0.1.7", path = "../axonos-spsc" }
+axonos-kernel-core = { version = "0.1.8", path = "../axonos-kernel-core" }
+axonos-time = { version = "0.1.8", path = "../axonos-time" }
+axonos-scheduler = { version = "0.1.8", path = "../axonos-scheduler" }
+axonos-capability = { version = "0.1.8", path = "../axonos-capability" }
+axonos-intent = { version = "0.1.8", path = "../axonos-intent" }
+axonos-spsc = { version = "0.1.8", path = "../axonos-spsc" }
 
 [[bin]]
 name = "axonos-firmware-stm32f407"

axonos-intent/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-intent"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
@@ -15,8 +15,8 @@ default = []
 std = ["axonos-time/std"]
 
 [dependencies]
-axonos-time = { version = "0.1.7", path = "../axonos-time" }
-axonos-capability = { version = "0.1.7", path = "../axonos-capability" }
+axonos-time = { version = "0.1.8", path = "../axonos-time" }
+axonos-capability = { version = "0.1.8", path = "../axonos-capability" }
 
 [lib]
 name = "axonos_intent"

axonos-kernel-core/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-kernel-core"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
@@ -15,11 +15,11 @@ default = []
 std = ["axonos-time/std", "axonos-intent/std"]
 
 [dependencies]
-axonos-spsc = { version = "0.1.7", path = "../axonos-spsc" }
-axonos-scheduler = { version = "0.1.7", path = "../axonos-scheduler" }
-axonos-capability = { version = "0.1.7", path = "../axonos-capability" }
-axonos-time = { version = "0.1.7", path = "../axonos-time" }
-axonos-intent = { version = "0.1.7", path = "../axonos-intent" }
+axonos-spsc = { version = "0.1.8", path = "../axonos-spsc" }
+axonos-scheduler = { version = "0.1.8", path = "../axonos-scheduler" }
+axonos-capability = { version = "0.1.8", path = "../axonos-capability" }
+axonos-time = { version = "0.1.8", path = "../axonos-time" }
+axonos-intent = { version = "0.1.8", path = "../axonos-intent" }
 
 [lib]
 name = "axonos_kernel_core"

axonos-scheduler/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-scheduler"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"

axonos-scheduler/kani-proofs/src/main.rs

@@ -33,9 +33,11 @@ fn sched_s1_admission_sound() {
     let c2: u32 = kani::any();
     let t2: u32 = kani::any();
 
-    // Constrain to reasonable BCI-scale parameters.
-    kani::assume(t1 > 0 && t1 <= 1_000_000);
-    kani::assume(t2 > 0 && t2 <= 1_000_000);
+    // Tight bounds: soundness proof is structural and does not require
+    // enumeration of large timer values. BCI epoch range is 4 ms, so 4_000 µs
+    // is the natural ceiling. Tight bounds keep the SAT problem tractable.
+    kani::assume(t1 > 0 && t1 <= 4_000);
+    kani::assume(t2 > 0 && t2 <= 4_000);
     kani::assume(c1 <= t1);
     kani::assume(c2 <= t2);
 
@@ -150,7 +152,8 @@ fn sched_s4_rta_single_task() {
     let c: u32 = kani::any();
     let t: u32 = kani::any();
 
-    kani::assume(t > 100 && t <= 1_000_000);
+    // Tight bounds for the same reason as S1.
+    kani::assume(t > 100 && t <= 4_000);
     kani::assume(c > 0 && c < t); // U < 1
     kani::assume(c <= t / 2); // keep below threshold so RTA converges in one step
 

axonos-spsc/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-spsc"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"

axonos-time/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "axonos-time"
-version = "0.1.7"
+version = "0.1.8"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"