Fix transaction closure bounds; replace Kani with no_panic checks

.github/workflows/ci.yml

@@ -0,0 +1,38 @@
+name: CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy, rustfmt
+      - run: cargo fmt --check
+      - run: cargo clippy
+      - run: cargo test
+
+  no-panic:
+    name: no-panic link check
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+      - run: cargo test --profile no-panic --features no-panic --test no_panic
+
+  msrv:
+    name: MSRV (1.77)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@1.77
+      # build only: dev-dependencies require a newer toolchain
+      - run: cargo build

CHANGELOG.md

@@ -1,3 +1,10 @@
+### 0.5.1 ###
+* :bug: `ReadCursor::transaction` closures can now return data borrowed from the input. See [#12](https://github.com/stepfunc/scursor/issues/12).
+* :bug: `WriteCursor::at_pos` now accepts `FnOnce` closures. See [#13](https://github.com/stepfunc/scursor/issues/13).
+* :wrench: Replaced the Kani proofs with link-time `no_panic` checks on every public routine, run in CI.
+* :wrench: Added round-trip property tests and a CI workflow.
+* Declared the minimum supported Rust version (1.77).
+
 ### 0.5.0 ###
 * :star: Optimized all integer and floating point read operations using the stabilized `slice::first_chunk` (Rust 1.77+).
 * :star: Added missing symmetric big-endian read/write routines for `u32`, `i32`, `f32`, `f64`, and `u48`.

Cargo.toml

@@ -3,6 +3,7 @@ name = "scursor"
 version = "0.5.0"
 license = "MIT OR Apache-2.0"
 edition = "2021"
+rust-version = "1.77"
 description = "Secure cursor library with support for read and write transactions"
 repository = "https://github.com/stepfunc/scursor"
 readme = "README.md"
@@ -14,7 +15,6 @@ unreachable_pub = "deny"
 trivial_casts = "deny"
 missing_docs = "deny"
 warnings = "deny"
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
 unused = { level = "deny", priority = -1 }
 missing_copy_implementations = "deny"
 
@@ -24,8 +24,21 @@ unwrap_used = "deny"
 expect_used = "deny"
 indexing_slicing = "deny"
 
+[dependencies]
+no-panic = { version = "0.1", optional = true }
+
 [dev-dependencies]
-kani = "0.0.1"
+proptest = "1"
 
+[features]
+# CI-only: fails to link if any public routine can panic. Requires an optimized
+# build (see the `no-panic` profile); debug builds will report false positives.
+no-panic = ["dep:no-panic"]
 
+[[test]]
+name = "no_panic"
+required-features = ["no-panic"]
 
+[profile.no-panic]
+inherits = "release"
+overflow-checks = true

README.md

@@ -59,24 +59,26 @@ fn main() {
 }
 ```
 
-## Formal Verification
+## Panic-freedom checks
 
-This library is formally verified to be panic-free using the [Kani Rust Verifier](https://model-checking.github.io/kani/). 
-Kani uses bit-precise model checking to mathematically prove the absence of panics, out-of-bounds 
-accesses, and overflows across all possible execution paths and inputs.
+When the `no-panic` feature is enabled, every public routine is annotated with
+[`no_panic`](https://github.com/dtolnay/no-panic). If the compiled code for a routine still contains a
+path that could panic, the check fails at link time. CI runs it with:
 
-To run the mathematical proofs yourself:
+```bash
+cargo test --profile no-panic --features no-panic --test no_panic
+```
 
-1. **Install Kani**:
-   ```bash
-   cargo install --locked kani-verifier
-   cargo kani setup
-   ```
+What the check does and doesn't tell you:
 
-2. **Run Verification**:
-   ```bash
-   cargo kani
-   ```
+* It covers every input, not a sample: it checks that no panic path survives in the compiled code.
+* It applies to the configuration that was checked: an optimized build (`opt-level = 3`) with
+  `overflow-checks = true` and `panic = "unwind"`. Debug builds and size-optimized builds keep
+  some unreachable panic paths, so the check reports false failures there. Those builds are
+  still panic-free; they just can't be checked this way.
+* The linker only examines code that is called, so `tests/no_panic.rs` calls every public routine.
+  `tests/no_panic_coverage.rs` fails if a routine is missing the annotation or the call.
+* The `no-panic` feature exists for this crate's CI. Don't enable it in your own builds.
 
 ## License
 Licensed under the terms of the MIT or Apache v2 licenses at your choice.

src/lib.rs

@@ -4,8 +4,5 @@
 mod read;
 mod write;
 
-#[cfg(kani)]
-mod proofs;
-
 pub use read::*;
 pub use write::*;