Use Dafny Fenwick library instead of my fenwick.rs port

Changes

4 changed files (+141/-11)

• Cargo.lock
  • @@ -15,6 +15,12 @@ "zerocopy",
    ] [[package]] + name = "autocfg" + version = "1.4.0" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" + + [[package]] name = "bitflags" version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index"
  • @@ -33,6 +39,22 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
    checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] + name = "dafny_runtime" + version = "0.1.0" + source = "git+https://git.unnamed.website/sdc#37365c164f4b3eb3ae0b12c30aac1ca9e5615a66" + dependencies = [ + "itertools", + "num", + "once_cell", + ] + + [[package]] + name = "either" + version = "1.15.0" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" + + [[package]] name = "fallible-iterator" version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index"
  • @@ -45,6 +67,14 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
    checksum = "7360491ce676a36bf9bb3c56c1aa791658183a54d2744120f27285738d90465a" [[package]] + name = "fenwick" + version = "0.1.0" + source = "git+https://git.unnamed.website/sdc#37365c164f4b3eb3ae0b12c30aac1ca9e5615a66" + dependencies = [ + "dafny_runtime", + ] + + [[package]] name = "getrandom" version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index"
  • @@ -74,6 +104,15 @@ "hashbrown",
    ] [[package]] + name = "itertools" + version = "0.11.0" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" + dependencies = [ + "either", + ] + + [[package]] name = "libc" version = "0.2.169" source = "registry+https://github.com/rust-lang/crates.io-index"
  • @@ -90,6 +129,79 @@ "vcpkg",
    ] [[package]] + name = "num" + version = "0.4.3" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23" + dependencies = [ + "num-bigint", + "num-complex", + "num-integer", + "num-iter", + "num-rational", + "num-traits", + ] + + [[package]] + name = "num-bigint" + version = "0.4.6" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" + dependencies = [ + "num-integer", + "num-traits", + ] + + [[package]] + name = "num-complex" + version = "0.4.6" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495" + dependencies = [ + "num-traits", + ] + + [[package]] + name = "num-integer" + version = "0.1.46" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" + dependencies = [ + "num-traits", + ] + + [[package]] + name = "num-iter" + version = "0.1.45" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "1429034a0490724d0075ebb2bc9e875d6503c3cf69e235a8941aa757d83ef5bf" + dependencies = [ + "autocfg", + "num-integer", + "num-traits", + ] + + [[package]] + name = "num-rational" + version = "0.4.2" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824" + dependencies = [ + "num-bigint", + "num-integer", + "num-traits", + ] + + [[package]] + name = "num-traits" + version = "0.2.19" + source = "registry+https://github.com/rust-lang/crates.io-index" + checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" + dependencies = [ + "autocfg", + ] + + [[package]] name = "once_cell" version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index"
  • @@ -176,6 +288,8 @@ [[package]]
    name = "sdrs" version = "0.1.0" dependencies = [ + "dafny_runtime", + "fenwick", "rand", "rusqlite", ]
• Cargo.toml
  • @@ -4,5 +4,7 @@ version = "0.1.0"
    edition = "2021" [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"
• src/fenwick.rs
  • @@ -1,5 +1,6 @@
    #![allow(dead_code)] + // Unused Rust port of // https://git.unnamed.website/sdc/plain/fenwick.c // Convert Vec in-place into Fenwick tree
• src/main.rs
  • @@ -1,5 +1,5 @@
    - mod fenwick; - + use dafny_runtime; + use fenwick::_module::fenwick; use rand::Rng; use rusqlite::{params, Connection, Result}; use std::env;
  • @@ -32,17 +32,23 @@
    // Get card weights let mut stmt = conn.prepare("SELECT weight FROM cards")?; let mut a = vec![0; n + 1]; - let mut f = vec![0; n + 1]; let mut sum = 0; for (i, w) in stmt.query_map([], |row| row.get::<_, i32>(0))?.enumerate() { let w = w?; a[i + 1] = w; - f[i + 1] = w; sum += w; } - fenwick::build(&mut f); + // Example for how to use Dafny-generated Rust: + // https://github.com/dafny-lang/dafny/blob/7bf2d6ad221df94c4a291b58e97a701da441dce0/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/arc/tokiouser-rust/src/main.rs + let obj = fenwick::_allocate_object(); + let seq = a[1..=n] + .into_iter() + .map(|x| dafny_runtime::DafnyInt::from_i32(x.clone())) + .collect(); + fenwick::_ctor(&obj, &seq); + let ft = dafny_runtime::rd!(obj); if verbose { println!("{:?}", &a[1..=n]);
  • @@ -70,7 +76,9 @@ loop {
    assert!(sum > 0); let s = rand::thread_rng().gen_range(0..sum); - let i = fenwick::search(&f, s) + 1; + // 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; if verbose { println!("{} {} {} {}", sum, s, i, a[i]);
  • @@ -84,7 +92,7 @@ Ok(())
    })?; if backend { - io::stdout().flush().unwrap(); + io::stdout().flush()?; } // Wait for confirmation
  • @@ -95,7 +103,8 @@ if b == 'q' {
    break; } if backend { - io::stdin().read_exact(&mut buf)?; // Skip newline + // Skip newline + io::stdin().read_exact(&mut buf)?; } stmt.query_row(params![i], |row| {
  • @@ -104,14 +113,15 @@ Ok(())
    })?; if backend { - io::stdout().flush().unwrap(); + io::stdout().flush()?; } // Read user input io::stdin().read_exact(&mut buf)?; let b = buf[0] as char; if backend { - io::stdin().read_exact(&mut buf)?; // Skip newline + // Skip newline + io::stdin().read_exact(&mut buf)?; } let w = match b {
  • @@ -121,7 +131,10 @@ _ => break,
    }; // Update Fenwick tree and database - fenwick::update(&mut f, i, w - a[i]); + ft.update( + &dafny_runtime::DafnyInt::from_usize(i), + &dafny_runtime::DafnyInt::from_i32(w - a[i]), + ); sum += w - a[i]; a[i] = w; conn.execute("UPDATE cards SET weight=? WHERE idx=?", params![w, i])?;