Koukyosyumei · Oct 23, 2026 · Oct 23, 2026 · Oct 23, 2026 · Oct 23, 2026
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,8 +1,13 @@
 [workspace]
 members = ["crates/*"]
 # The h5i-app examples are their own workspace, depending on the h5i-app
-# crates by path as an application would.
-exclude = ["examples/app", "crates/h5i-app-gpu"]
+# crates by path as an application would. The GPU backends need CUDA and git
+# dependencies, so they build separately too.
+exclude = [
+    "examples/app",
+    "crates/h5i-app-gpu/backend-nvvm",
+    "crates/h5i-app-gpu/backend-oxide",
+]
 resolver = "3"
 
 # Shared dependency versions for every workspace crate — a single source of
@@ -24,15 +29,15 @@ sha2 = "0.10"
 # crates publish against each other. External dependencies are declared in
 # each crate, not here: a user's build of h5i-app must not inherit the h5i
 # CLI's feature choices (serde_json's `preserve_order`, for one).
-h5i-app-core = { path = "crates/h5i-app-core", version = "0.1.2" }
-h5i-app-http = { path = "crates/h5i-app-http", version = "0.1.2" }
-h5i-app-json = { path = "crates/h5i-app-json", version = "0.1.2" }
-h5i-app-pg = { path = "crates/h5i-app-pg", version = "0.1.2" }
-h5i-app-pgsql = { path = "crates/h5i-app-pgsql", version = "0.1.2" }
-h5i-app-schema = { path = "crates/h5i-app-schema", version = "0.1.2" }
-h5i-app-sql = { path = "crates/h5i-app-sql", version = "0.1.2" }
-h5i-app-std = { path = "crates/h5i-app-std", version = "0.1.2" }
-h5i-app-token = { path = "crates/h5i-app-token", version = "0.1.2" }
+h5i-app-core = { path = "crates/h5i-app-core", version = "0.1.3" }
+h5i-app-http = { path = "crates/h5i-app-http", version = "0.1.3" }
+h5i-app-json = { path = "crates/h5i-app-json", version = "0.1.3" }
+h5i-app-pg = { path = "crates/h5i-app-pg", version = "0.1.3" }
+h5i-app-pgsql = { path = "crates/h5i-app-pgsql", version = "0.1.3" }
+h5i-app-schema = { path = "crates/h5i-app-schema", version = "0.1.3" }
+h5i-app-sql = { path = "crates/h5i-app-sql", version = "0.1.3" }
+h5i-app-std = { path = "crates/h5i-app-std", version = "0.1.3" }
+h5i-app-token = { path = "crates/h5i-app-token", version = "0.1.3" }
 
 # The repo's primary product is the `h5i` binary, so it lives at the root
 # (`cargo install --path .` / `cargo run` do the obvious thing). The library it

diff --git a/README.md b/README.md
@@ -36,7 +36,7 @@ npx skills add h5i-dev/h5i
 
 ```toml
 [dependencies]
-h5i-app = { version = "0.1.2", features = ["http", "postgres"] }
+h5i-app = { version = "0.1.3", features = ["http", "postgres"] }
 ```
 
 <p align="center">

diff --git a/crates/h5i-app-cli/Cargo.toml b/crates/h5i-app-cli/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-cli"
 description = "`h5i app`: extract an h5i-app kernel to Lean, gate its proofs, and test the spec with mutants"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 publish = false
 
 # The whole development loop of an h5i-app application, behind one command

diff --git a/crates/h5i-app-core/Cargo.toml b/crates/h5i-app-core/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-core"
 description = "Core contract between a verified h5i-app kernel and its untrusted shell"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-gpu/Cargo.toml b/crates/h5i-app-gpu/Cargo.toml
@@ -1,10 +1,6 @@
 [package]
 name = "h5i-app-gpu"
-version = "0.1.2"
+version = "0.1.3"
 edition = "2024"
 license = "Apache-2.0"
 description = "Optional batch execution adapters and differential checks for application kernels"
-[workspace]
-members = ["backend-nvvm"]
-default-members = ["."]
-exclude = ["backend-oxide"]
diff --git a/crates/h5i-app-gpu/Cargo.lock → crates/h5i-app-gpu/backend-nvvm/Cargo.lock b/crates/h5i-app-gpu/Cargo.lock → crates/h5i-app-gpu/backend-nvvm/Cargo.lock
diff --git a/crates/h5i-app-gpu/backend-oxide/Cargo.lock b/crates/h5i-app-gpu/backend-oxide/Cargo.lock
diff --git a/crates/h5i-app-gpu/backend-oxide/Cargo.toml b/crates/h5i-app-gpu/backend-oxide/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "h5i-app-gpu-backend-oxide"
-version = "0.1.2"
+version = "0.1.0"
 edition = "2024"
 license = "Apache-2.0"
 publish = false

diff --git a/crates/h5i-app-http/Cargo.toml b/crates/h5i-app-http/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-http"
 description = "HTTP shell for h5i-app kernels: authentication and input decoding (trusted), dispatch to the engine"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-json/Cargo.toml b/crates/h5i-app-json/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-json"
 description = "JSON writer for h5i-app replies, extracted to Lean and proven"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-mem/Cargo.toml b/crates/h5i-app-mem/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "h5i-app-mem"
-version = "0.1.2"
+version = "0.1.3"
 edition = "2024"
 license = "Apache-2.0"
 description = "Single-owner RAM read cache with PostgreSQL write-through execution"

diff --git a/crates/h5i-app-pg/Cargo.toml b/crates/h5i-app-pg/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-pg"
 description = "PostgreSQL engine for h5i-app: tenant-scoped snapshots, SERIALIZABLE execution with retry, idempotency"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-pgsql/Cargo.toml b/crates/h5i-app-pgsql/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-pgsql"
 description = "PostgreSQL text for h5i-app's planned statements; extracted to Lean and proven to mean what the planner's statements mean"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-schema/Cargo.toml b/crates/h5i-app-schema/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-schema"
 description = "Declare kernel row types once; get the structs and their table mappings"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-sql/Cargo.toml b/crates/h5i-app-sql/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-sql"
 description = "Pure planner from h5i-app write sets to keyed SQL statements; extracted to Lean and proven"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-std/Cargo.toml b/crates/h5i-app-std/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-std"
 description = "Byte strings, sets and maps for h5i-app kernels, extracted to Lean and proven"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-token/Cargo.toml b/crates/h5i-app-token/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-token"
 description = "Bearer token encoding and parsing for h5i-app, extracted to Lean and proven"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 repository = "https://github.com/h5i-dev/h5i"
 homepage = "https://github.com/h5i-dev/h5i"
 readme = "../h5i-app/README.md"

diff --git a/crates/h5i-app-xtask/Cargo.toml b/crates/h5i-app-xtask/Cargo.toml
@@ -3,7 +3,7 @@ name = "h5i-app-xtask"
 description = "Repository checks: `cargo app-verify`, and `cargo app` for `h5i app` without the browser build"
 edition = "2024"
 license = "Apache-2.0"
-version = "0.1.2"
+version = "0.1.3"
 publish = false
 
 [dependencies]

diff --git a/crates/h5i-app/Cargo.toml b/crates/h5i-app/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "h5i-app"
-version = "0.1.2"
+version = "0.1.3"
 edition = "2024"
 license = "Apache-2.0"
 repository = "https://github.com/h5i-dev/h5i"

diff --git a/docs/app/GPU.md b/docs/app/GPU.md
@@ -135,7 +135,7 @@ device compilation probe without the failing host runtime.
 
 ## Earlier calculator / Result failures
 
-`crates/h5i-app-gpu` is a separate workspace/toolchain invocation, excluded from
+`crates/h5i-app-gpu/backend-oxide` is a separate workspace/toolchain invocation, excluded from
 normal extraction and builds. Its default CPU test calls the existing
 calculator kernel's `compute`, including checked arithmetic errors. The
 `calculator-probe` feature adds a thin `#[kernel]` batch wrapper with separate

diff --git a/examples/app/Cargo.lock b/examples/app/Cargo.lock