Update deps, add fenwick benchmark script The Dafny-generated code is so freaking slow 😭

Changes

4 changed files (+80/-59)

• Cargo.lock
  • @@ -3,18 +3,6 @@ # It is not intended for manual editing.
    version = 4 [[package]] - name = "ahash" - version = "0.8.11" - source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" - dependencies = [ - "cfg-if", - "once_cell", - "version_check", - "zerocopy 0.7.35", - ] - - [[package]] name = "autocfg" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index"
  • @@ -69,30 +57,37 @@ "dafny_runtime",
    ] [[package]] + name = "foldhash" + version = "0.1.5" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" + + [[package]] name = "getrandom" - version = "0.2.15" + version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" + checksum = "73fea8450eea4bac3940448fb7ae50d91f034f941199fcd9d909a5a07aa455f0" dependencies = [ "cfg-if", "libc", + "r-efi", "wasi", ] [[package]] name = "hashbrown" - version = "0.14.5" + version = "0.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" + checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" dependencies = [ - "ahash", + "foldhash", ] [[package]] name = "hashlink" - version = "0.9.1" + version = "0.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af" + checksum = "7382cf6263419f2d8df38c55d7da83da5c18aef87fc7a7fc1fb1e344edfe14c1" dependencies = [ "hashbrown", ]
  • @@ -114,9 +109,9 @@ checksum = "c19937216e9d3aa9956d9bb8dfc0b0c8beb6058fc4f7a4dc4d850edf86a237d6"
    [[package]] name = "libsqlite3-sys" - version = "0.30.1" + version = "0.32.0" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "2e99fb7a497b1e3339bc746195567ed8d3e24945ecd636e3619d20b9de9e9149" + checksum = "fbb8270bb4060bd76c6e96f20c52d80620f1d82a3470885694e41e0f81ef6fe7" dependencies = [ "pkg-config", "vcpkg",
  • @@ -213,7 +208,7 @@ version = "0.2.21"
    source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" dependencies = [ - "zerocopy 0.8.24", + "zerocopy", ] [[package]]
  • @@ -235,21 +230,27 @@ "proc-macro2",
    ] [[package]] + name = "r-efi" + version = "5.2.0" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "74765f6d916ee2faa39bc8e68e4f3ed8949b48cccdac59983d287a7cb71ce9c5" + + [[package]] name = "rand" - version = "0.8.5" + version = "0.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" + checksum = "3779b94aeb87e8bd4e834cee3650289ee9e0d5677f976ecdb6d219e5f4f6cd94" dependencies = [ - "libc", "rand_chacha", "rand_core", + "zerocopy", ] [[package]] name = "rand_chacha" - version = "0.3.1" + version = "0.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" + checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" dependencies = [ "ppv-lite86", "rand_core",
  • @@ -257,18 +258,18 @@ ]
    [[package]] name = "rand_core" - version = "0.6.4" + version = "0.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" + checksum = "99d9a13982dcf210057a8a78572b2217b667c3beacbf3a0d8b454f6f82837d38" dependencies = [ "getrandom", ] [[package]] name = "rusqlite" - version = "0.32.1" + version = "0.34.0" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "7753b721174eb8ff87a9a0e799e2d7bc3749323e773db92e0984debb00019d6e" + checksum = "37e34486da88d8e051c7c0e23c3f15fd806ea8546260aa2fec247e97242ec143" dependencies = [ "bitflags", "fallible-iterator",
  • @@ -318,24 +319,21 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
    checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426" [[package]] - name = "version_check" - version = "0.9.5" - source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - - [[package]] name = "wasi" - version = "0.11.0+wasi-snapshot-preview1" + version = "0.14.2+wasi-0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" + checksum = "9683f9a5a998d873c0d21fcbe3c083009670149a8fab228644b8bd36b2c48cb3" + dependencies = [ + "wit-bindgen-rt", + ] [[package]] - name = "zerocopy" - version = "0.7.35" + name = "wit-bindgen-rt" + version = "0.39.0" source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" + checksum = "6f42320e61fe2cfd34354ecb597f86f413484a798ba44a8ca1165c58d42da6c1" dependencies = [ - "zerocopy-derive 0.7.35", + "bitflags", ] [[package]]
  • @@ -344,18 +342,7 @@ version = "0.8.24"
    source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2586fea28e186957ef732a5f8b3be2da217d65c5969d4b1e17f973ebbe876879" dependencies = [ - "zerocopy-derive 0.8.24", - ] - - [[package]] - name = "zerocopy-derive" - version = "0.7.35" - source = "registry+https://github.com/rust-lang/crates.io-index" - checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" - dependencies = [ - "proc-macro2", - "quote", - "syn", + "zerocopy-derive", ] [[package]]
• Cargo.toml
  • @@ -2,9 +2,14 @@ [package]
    name = "sdrs" version = "0.1.0" edition = "2021" + default-run = "sdrs" [dependencies] dafny_runtime = { git = "https://git.unnamed.website/sdc", version = "0.1.0" } fenwick = { git = "https://git.unnamed.website/sdc", version = "0.1.0" } - rand = "0.8.5" - rusqlite = "0.32.1" + rand = "0.9.0" + rusqlite = "0.34.0" + + [[bin]] + name = "fenwicktest" + path = "src/fenwicktest.rs"
• src/fenwicktest.rs (new)
  • @@ -0,0 +1,30 @@
    + use fenwick::_module::fenwick; + use std::time::Instant; + + fn main() { + const N: usize = 1 << 17; + let a = rand::random_iter::<i32>() + .take(N) + .map(|x| dafny_runtime::DafnyInt::from_i32(x % 1000)) + .collect(); + let obj = fenwick::_allocate_object(); + fenwick::_ctor(&obj, &a); + let ft = dafny_runtime::rd!(obj); + + const T: usize = 1 << 12; + + let test: Vec<_> = rand::random_iter::<i32>().zip(rand::random_iter::<i32>()) + .take(T) + .map(|x| (x.0 as usize % N + 1, x.1 as usize % N + 1)) + .map(|x| if x.0 > x.1 { (x.1, x.0) } else { x }) + .map(|x| (dafny_runtime::DafnyInt::from_usize(x.0), dafny_runtime::DafnyInt::from_usize(x.1))) + .collect(); + + println!("starting benchmark"); + let now = Instant::now(); + for (i, j) in &test { + ft.range_query(i, j); + } + let elapsed = now.elapsed().as_micros(); + println!("fast range query took {} µs", elapsed); + }
• src/main.rs
  • @@ -1,5 +1,4 @@
    use fenwick::_module::fenwick; - use rand::Rng; use rusqlite::{params, Connection, Result}; use std::env; use std::error::Error;
  • @@ -74,7 +73,7 @@
    loop { assert!(sum > 0); - let s = rand::thread_rng().gen_range(0..sum); + let s = rand::random_range(0..sum); // ft is 0-indexed so we need to add 1 // Not sure why there's only as_usize() and not as_i32() let i = ft.search(&dafny_runtime::DafnyInt::from_i32(s)).as_usize() + 1;