From e7c3f72fbf94f5420d04980cbe714eec99dd3ea9 Mon Sep 17 00:00:00 2001 From: unldenis Date: Mon, 22 Sep 2025 12:41:56 +0200 Subject: [PATCH 1/2] Init Kani --- Cargo.toml | 4 ++ kani/.gitignore | 1 + kani/Cargo.lock | 143 +++++++++++++++++++++++++++++++++++++++++++++++ kani/Cargo.toml | 10 ++++ kani/src/main.rs | 13 +++++ 5 files changed, 171 insertions(+) create mode 100644 kani/.gitignore create mode 100644 kani/Cargo.lock create mode 100644 kani/Cargo.toml create mode 100644 kani/src/main.rs diff --git a/Cargo.toml b/Cargo.toml index cef5853..be586a5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -21,3 +21,7 @@ default = ["debug", "satisfy"] # Enable Debug trait implementations for error types debug = [] satisfy = [] +kani = [] + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(loom)', 'cfg(fuzzing)'] } diff --git a/kani/.gitignore b/kani/.gitignore new file mode 100644 index 0000000..1de5659 --- /dev/null +++ b/kani/.gitignore @@ -0,0 +1 @@ +target \ No newline at end of file diff --git a/kani/Cargo.lock b/kani/Cargo.lock new file mode 100644 index 0000000..3c83a5f --- /dev/null +++ b/kani/Cargo.lock @@ -0,0 +1,143 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "arrayvec" +version = "0.7.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" + +[[package]] +name = "base58ck" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2c8d66485a3a2ea485c1913c4572ce0256067a5377ac8c75c4960e1cda98605f" +dependencies = [ + "bitcoin-internals", + "bitcoin_hashes", +] + +[[package]] +name = "bech32" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d965446196e3b7decd44aa7ee49e31d630118f90ef12f97900f262eb915c951d" + +[[package]] +name = "bitcoin" +version = "0.32.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda569d741b895131a88ee5589a467e73e9c4718e958ac9308e4f7dc44b6945" +dependencies = [ + "base58ck", + "bech32", + "bitcoin-internals", + "bitcoin-io", + "bitcoin-units", + "bitcoin_hashes", + "hex-conservative", + "hex_lit", + "secp256k1", +] + +[[package]] +name = "bitcoin-internals" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "30bdbe14aa07b06e6cfeffc529a1f099e5fbe249524f8125358604df99a4bed2" + +[[package]] +name = "bitcoin-io" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b47c4ab7a93edb0c7198c5535ed9b52b63095f4e9b45279c6736cec4b856baf" + +[[package]] +name = "bitcoin-units" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5285c8bcaa25876d07f37e3d30c303f2609179716e11d688f51e8f1fe70063e2" +dependencies = [ + "bitcoin-internals", +] + +[[package]] +name = "bitcoin_hashes" +version = "0.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb18c03d0db0247e147a21a6faafd5a7eb851c743db062de72018b6b7e8e4d16" +dependencies = [ + "bitcoin-io", + "hex-conservative", +] + +[[package]] +name = "cc" +version = "1.2.38" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "80f41ae168f955c12fb8960b057d70d0ca153fb83182b57d86380443527be7e9" +dependencies = [ + "find-msvc-tools", + "shlex", +] + +[[package]] +name = "find-msvc-tools" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ced73b1dacfc750a6db6c0a0c3a3853c8b41997e2e2c563dc90804ae6867959" + +[[package]] +name = "hex-conservative" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5313b072ce3c597065a808dbf612c4c8e8590bdbf8b579508bf7a762c5eae6cd" +dependencies = [ + "arrayvec", +] + +[[package]] +name = "hex_lit" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3011d1213f159867b13cfd6ac92d2cd5f1345762c63be3554e84092d85a50bbd" + +[[package]] +name = "kani" +version = "0.1.0" +dependencies = [ + "tinyminiscript", +] + +[[package]] +name = "secp256k1" +version = "0.29.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9465315bc9d4566e1724f0fffcbcc446268cb522e60f9a27bcded6b19c108113" +dependencies = [ + "bitcoin_hashes", + "secp256k1-sys", +] + +[[package]] +name = "secp256k1-sys" +version = "0.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d4387882333d3aa8cb20530a17c69a3752e97837832f34f6dccc760e715001d9" +dependencies = [ + "cc", +] + +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "tinyminiscript" +version = "0.0.4" +dependencies = [ + "bitcoin", +] diff --git a/kani/Cargo.toml b/kani/Cargo.toml new file mode 100644 index 0000000..aa10cb2 --- /dev/null +++ b/kani/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "kani" +version = "0.1.0" +edition = "2024" + +[dependencies] + + +[dependencies.tinyminiscript] +path = ".." \ No newline at end of file diff --git a/kani/src/main.rs b/kani/src/main.rs new file mode 100644 index 0000000..ece1460 --- /dev/null +++ b/kani/src/main.rs @@ -0,0 +1,13 @@ +fn main() { + println!("Hello, world!"); +} + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + pub fn check_something() { + assert!(1 == 2) + } +} From fa9837d410de552a1492b153c32dcdb8cbd530fe Mon Sep 17 00:00:00 2001 From: unldenis Date: Mon, 22 Sep 2025 14:47:51 +0200 Subject: [PATCH 2/2] Fix use of unresolved module or unlinked crate `std` --- Cargo.toml | 2 +- src/parser/mod.rs | 13 +++++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index be586a5..d8a7ef7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,7 +11,7 @@ categories = ["cryptography", "parsing"] readme = "README.md" [dependencies] -bitcoin = { version = "0.32.7", default-features = false } +bitcoin = { version = "0.32.7", default-features = true } [lib] crate-type = ["lib"] diff --git a/src/parser/mod.rs b/src/parser/mod.rs index e9fd0b0..8dc0e8c 100644 --- a/src/parser/mod.rs +++ b/src/parser/mod.rs @@ -1208,3 +1208,16 @@ fn parse_bool<'a>(ctx: &mut ParserContext<'a>) -> Result> { } } } + + + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + pub fn check_something() { + let ctx = parse("wsh(or_d(pk({}),older(12960)))"); + assert!(ctx.is_ok()); + } +} \ No newline at end of file