From b7072c5017d41abcc8b12252947ae6c74e1b0295 Mon Sep 17 00:00:00 2001 From: Julian Date: Fri, 14 Aug 2026 10:25:11 -0400 Subject: [PATCH 01/13] work toward generating sanity rules for soroban and compiling it --- Cargo.toml | 2 +- cvlr-asserts/src/core.rs | 1 + cvlr-asserts/src/log.rs | 1 + cvlr-log/src/core.rs | 3 ++- cvlr-mathint/src/nativeint_u64.rs | 1 + cvlr-nondet/src/scalars.rs | 1 + cvlr-spec/src/lib.rs | 1 + cvlr/src/u128_arith.rs | 1 + 8 files changed, 9 insertions(+), 2 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index aadb351..166bd12 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -51,7 +51,7 @@ syn = "2" macrotest = "1" trybuild = "1" -cvlr = { path = "cvlr", version = "=0.6.1" } +cvlr = { path = "cvlr", default-features = false, version = "=0.6.1" } cvlr-asserts = { path = "cvlr-asserts", version = "=0.6.1" } cvlr-mathint = { path = "cvlr-mathint", version = "=0.6.1" } cvlr-nondet = { path = "cvlr-nondet", default-features = false, version = "=0.6.1" } diff --git a/cvlr-asserts/src/core.rs b/cvlr-asserts/src/core.rs index d532f19..7f36c81 100644 --- a/cvlr-asserts/src/core.rs +++ b/cvlr-asserts/src/core.rs @@ -1,4 +1,5 @@ mod rt_decls { + #[link(wasm_import_module = "env")] extern "C" { pub fn CVT_assume(_c: bool); pub fn CVT_assert(_c: bool); diff --git a/cvlr-asserts/src/log.rs b/cvlr-asserts/src/log.rs index 040c0cc..629900a 100644 --- a/cvlr-asserts/src/log.rs +++ b/cvlr-asserts/src/log.rs @@ -1,4 +1,5 @@ mod rt_decls { + #[link(wasm_import_module = "env")] extern "C" { #![allow(improper_ctypes)] // duplicated to avoid cvlr-assert depend on any other cvlr crate diff --git a/cvlr-log/src/core.rs b/cvlr-log/src/core.rs index f30f92a..6692244 100644 --- a/cvlr-log/src/core.rs +++ b/cvlr-log/src/core.rs @@ -1,5 +1,6 @@ pub mod rt_decls { - #[allow(improper_ctypes)] + #[link(wasm_import_module = "env")] + #[allow(improper_ctypes)] extern "C" { pub fn CVT_calltrace_print_tag(tag: &str); diff --git a/cvlr-mathint/src/nativeint_u64.rs b/cvlr-mathint/src/nativeint_u64.rs index b6d6994..eb57d91 100644 --- a/cvlr-mathint/src/nativeint_u64.rs +++ b/cvlr-mathint/src/nativeint_u64.rs @@ -12,6 +12,7 @@ pub struct NativeIntU64(u64); mod rt_decls { type BoolU64 = u64; + #[link(wasm_import_module = "env")] extern "C" { pub fn CVT_nativeint_u64_eq(_: u64, _: u64) -> BoolU64; pub fn CVT_nativeint_u64_lt(_: u64, _: u64) -> BoolU64; diff --git a/cvlr-nondet/src/scalars.rs b/cvlr-nondet/src/scalars.rs index 4250db3..867e55f 100644 --- a/cvlr-nondet/src/scalars.rs +++ b/cvlr-nondet/src/scalars.rs @@ -1,6 +1,7 @@ use crate::Nondet; mod rt_decls { + #[link(wasm_import_module = "env")] #[allow(improper_ctypes)] extern "C" { // Definition of external functions that represent getting arbitrary values diff --git a/cvlr-spec/src/lib.rs b/cvlr-spec/src/lib.rs index 5af3123..4da123c 100644 --- a/cvlr-spec/src/lib.rs +++ b/cvlr-spec/src/lib.rs @@ -53,6 +53,7 @@ //! // Define a simple spec - cvlr_true uses eval_with_states for ensures //! let spec = cvlr_spec(cvlr_true::(), cvlr_true::()); //! ``` +#![no_std] mod combinators; mod formula; diff --git a/cvlr/src/u128_arith.rs b/cvlr/src/u128_arith.rs index 63de700..f25ec23 100644 --- a/cvlr/src/u128_arith.rs +++ b/cvlr/src/u128_arith.rs @@ -1,4 +1,5 @@ mod rt_decls { + #[link(wasm_import_module = "env")] #[allow(improper_ctypes)] extern "C" { pub fn CVT_u128_leq(x: u128, y: u128) -> bool; From 85fef5ff805d665fda8ccac7400891480db80377 Mon Sep 17 00:00:00 2001 From: Julian Date: Tue, 25 Aug 2026 18:02:30 -0400 Subject: [PATCH 02/13] export some primitives for use in cvlr_soroban --- cvlr-nondet/src/lib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cvlr-nondet/src/lib.rs b/cvlr-nondet/src/lib.rs index b386c9a..0418277 100644 --- a/cvlr-nondet/src/lib.rs +++ b/cvlr-nondet/src/lib.rs @@ -13,4 +13,5 @@ pub mod havoc; pub use core::{nondet, nondet_with, Nondet}; pub use option::nondet_option; -pub use scalars::{cvlr_nondet_small_i128, cvlr_nondet_small_u128}; +pub use scalars::{cvlr_nondet_small_i128, cvlr_nondet_small_u128, + cvlr_nondet_u64, cvlr_nondet_u32}; From 34e159df21d308b20809d0fe7e199fc0b0d362ee Mon Sep 17 00:00:00 2001 From: Julian Date: Wed, 26 Aug 2026 16:35:34 -0400 Subject: [PATCH 03/13] clean up 'env' --- cvlr-asserts/src/core.rs | 5 ++++- cvlr-asserts/src/log.rs | 5 ++++- cvlr-log/src/core.rs | 5 ++++- cvlr-mathint/src/nativeint_u64.rs | 5 ++++- cvlr-nondet/src/scalars.rs | 5 ++++- cvlr/src/u128_arith.rs | 5 ++++- 6 files changed, 24 insertions(+), 6 deletions(-) diff --git a/cvlr-asserts/src/core.rs b/cvlr-asserts/src/core.rs index 7f36c81..22f95df 100644 --- a/cvlr-asserts/src/core.rs +++ b/cvlr-asserts/src/core.rs @@ -1,5 +1,8 @@ mod rt_decls { - #[link(wasm_import_module = "env")] + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "cvlr") + )] extern "C" { pub fn CVT_assume(_c: bool); pub fn CVT_assert(_c: bool); diff --git a/cvlr-asserts/src/log.rs b/cvlr-asserts/src/log.rs index 629900a..036aeab 100644 --- a/cvlr-asserts/src/log.rs +++ b/cvlr-asserts/src/log.rs @@ -1,5 +1,8 @@ mod rt_decls { - #[link(wasm_import_module = "env")] + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "cvlr") + )] extern "C" { #![allow(improper_ctypes)] // duplicated to avoid cvlr-assert depend on any other cvlr crate diff --git a/cvlr-log/src/core.rs b/cvlr-log/src/core.rs index 6692244..04f7de5 100644 --- a/cvlr-log/src/core.rs +++ b/cvlr-log/src/core.rs @@ -1,5 +1,8 @@ pub mod rt_decls { - #[link(wasm_import_module = "env")] + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "cvlr") + )] #[allow(improper_ctypes)] extern "C" { pub fn CVT_calltrace_print_tag(tag: &str); diff --git a/cvlr-mathint/src/nativeint_u64.rs b/cvlr-mathint/src/nativeint_u64.rs index eb57d91..248e168 100644 --- a/cvlr-mathint/src/nativeint_u64.rs +++ b/cvlr-mathint/src/nativeint_u64.rs @@ -12,7 +12,10 @@ pub struct NativeIntU64(u64); mod rt_decls { type BoolU64 = u64; - #[link(wasm_import_module = "env")] + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "cvlr") + )] extern "C" { pub fn CVT_nativeint_u64_eq(_: u64, _: u64) -> BoolU64; pub fn CVT_nativeint_u64_lt(_: u64, _: u64) -> BoolU64; diff --git a/cvlr-nondet/src/scalars.rs b/cvlr-nondet/src/scalars.rs index 867e55f..ed6d901 100644 --- a/cvlr-nondet/src/scalars.rs +++ b/cvlr-nondet/src/scalars.rs @@ -1,7 +1,10 @@ use crate::Nondet; mod rt_decls { - #[link(wasm_import_module = "env")] + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "cvlr") + )] #[allow(improper_ctypes)] extern "C" { // Definition of external functions that represent getting arbitrary values diff --git a/cvlr/src/u128_arith.rs b/cvlr/src/u128_arith.rs index f25ec23..45c267f 100644 --- a/cvlr/src/u128_arith.rs +++ b/cvlr/src/u128_arith.rs @@ -1,5 +1,8 @@ mod rt_decls { - #[link(wasm_import_module = "env")] + #[cfg_attr( + all(target_family = "wasm", target_os = "none"), + link(wasm_import_module = "cvlr") + )] #[allow(improper_ctypes)] extern "C" { pub fn CVT_u128_leq(x: u128, y: u128) -> bool; From a579210bb92c3abecb282cff918ef24fa2d2c07f Mon Sep 17 00:00:00 2001 From: Julian Date: Wed, 26 Aug 2026 16:37:51 -0400 Subject: [PATCH 04/13] remove duplicate annotation --- cvlr-spec/src/lib.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/cvlr-spec/src/lib.rs b/cvlr-spec/src/lib.rs index ccdeefb..2d535eb 100644 --- a/cvlr-spec/src/lib.rs +++ b/cvlr-spec/src/lib.rs @@ -54,7 +54,6 @@ //! // Define a simple spec - cvlr_true uses eval_with_states for ensures //! let spec = cvlr_spec(cvlr_true::(), cvlr_true::()); //! ``` -#![no_std] mod combinators; mod formula; From fc92ab0799bdbb46576a1ed0247adad5bc2f7378 Mon Sep 17 00:00:00 2001 From: Julian Date: Wed, 26 Aug 2026 16:39:31 -0400 Subject: [PATCH 05/13] fmt --- cvlr-log/src/core.rs | 2 +- cvlr-nondet/src/lib.rs | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/cvlr-log/src/core.rs b/cvlr-log/src/core.rs index 04f7de5..09f0e4a 100644 --- a/cvlr-log/src/core.rs +++ b/cvlr-log/src/core.rs @@ -3,7 +3,7 @@ pub mod rt_decls { all(target_family = "wasm", target_os = "none"), link(wasm_import_module = "cvlr") )] - #[allow(improper_ctypes)] + #[allow(improper_ctypes)] extern "C" { pub fn CVT_calltrace_print_tag(tag: &str); diff --git a/cvlr-nondet/src/lib.rs b/cvlr-nondet/src/lib.rs index 0418277..36d6f14 100644 --- a/cvlr-nondet/src/lib.rs +++ b/cvlr-nondet/src/lib.rs @@ -13,5 +13,6 @@ pub mod havoc; pub use core::{nondet, nondet_with, Nondet}; pub use option::nondet_option; -pub use scalars::{cvlr_nondet_small_i128, cvlr_nondet_small_u128, - cvlr_nondet_u64, cvlr_nondet_u32}; +pub use scalars::{ + cvlr_nondet_small_i128, cvlr_nondet_small_u128, cvlr_nondet_u32, cvlr_nondet_u64, +}; From ea27c3ad28695c0af40104a6c3242e603168f644 Mon Sep 17 00:00:00 2001 From: Julian Date: Wed, 26 Aug 2026 16:41:26 -0400 Subject: [PATCH 06/13] remove default-features=false --- Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index 166bd12..aadb351 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -51,7 +51,7 @@ syn = "2" macrotest = "1" trybuild = "1" -cvlr = { path = "cvlr", default-features = false, version = "=0.6.1" } +cvlr = { path = "cvlr", version = "=0.6.1" } cvlr-asserts = { path = "cvlr-asserts", version = "=0.6.1" } cvlr-mathint = { path = "cvlr-mathint", version = "=0.6.1" } cvlr-nondet = { path = "cvlr-nondet", default-features = false, version = "=0.6.1" } From c4891c17f015857d47cab8a5cd93969291938f71 Mon Sep 17 00:00:00 2001 From: Chandrakana Nandi Date: Wed, 26 Aug 2026 14:15:57 -0700 Subject: [PATCH 07/13] trying to fix CI based on copilot advice --- .github/workflows/main.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8f237ec..442ec6d 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -45,3 +45,5 @@ jobs: run: cargo install cargo-expand - name: Run cargo test run: cargo test --verbose + - name: Run cvlr-hook tests + run: cargo test -p cvlr-hook --test tests -- --test-threads=1 From deb969fe453741b1e0d4159844434582ad23063b Mon Sep 17 00:00:00 2001 From: Chandrakana Nandi Date: Wed, 26 Aug 2026 14:19:52 -0700 Subject: [PATCH 08/13] forgot to exclude hook tests from all tests --- .github/workflows/main.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 442ec6d..735256f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -43,7 +43,7 @@ jobs: toolchain: stable - name: Install cargo-expand run: cargo install cargo-expand - - name: Run cargo test - run: cargo test --verbose - - name: Run cvlr-hook tests + - name: Run cargo test (excluding cvlr-hook) + run: cargo test --verbose --exclude cvlr-hook + - name: Run cvlr-hook tests serially run: cargo test -p cvlr-hook --test tests -- --test-threads=1 From 428ce77c55cfba5f04092a8b2361d8465c046f79 Mon Sep 17 00:00:00 2001 From: Chandrakana Nandi Date: Wed, 26 Aug 2026 14:24:19 -0700 Subject: [PATCH 09/13] add workspace --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 735256f..5164e9d 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -44,6 +44,6 @@ jobs: - name: Install cargo-expand run: cargo install cargo-expand - name: Run cargo test (excluding cvlr-hook) - run: cargo test --verbose --exclude cvlr-hook + run: cargo test --verbose --workspace --exclude cvlr-hook - name: Run cvlr-hook tests serially run: cargo test -p cvlr-hook --test tests -- --test-threads=1 From d55fd8be565e21bdfdafbea7ea4469f040b08ab7 Mon Sep 17 00:00:00 2001 From: Chandrakana Nandi Date: Wed, 26 Aug 2026 15:20:32 -0700 Subject: [PATCH 10/13] avoid builtin macros that affect expansion across rustc versions --- .../expand/test_hook_combined.expanded.rs | 53 +++++----------- cvlr-hook/tests/expand/test_hook_combined.rs | 44 ++++++++----- .../tests/expand/test_hook_end.expanded.rs | 62 +++---------------- cvlr-hook/tests/expand/test_hook_end.rs | 21 +++++-- .../tests/expand/test_hook_start.expanded.rs | 7 ++- cvlr-hook/tests/expand/test_hook_start.rs | 11 +++- 6 files changed, 83 insertions(+), 115 deletions(-) diff --git a/cvlr-hook/tests/expand/test_hook_combined.expanded.rs b/cvlr-hook/tests/expand/test_hook_combined.expanded.rs index 9b3ba08..14693c1 100644 --- a/cvlr-hook/tests/expand/test_hook_combined.expanded.rs +++ b/cvlr-hook/tests/expand/test_hook_combined.expanded.rs @@ -5,68 +5,45 @@ fn hook_start() { fn hook_end() { (); } +fn check_eq(_a: i32, _b: i32) { + (); +} +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} +fn log(_msg: &str) { + (); +} fn tmp() -> Result<()> { hook_start(); hook_end(); Ok(()) } fn t3() { - match (&tmp(), &Ok(())) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_res(tmp(), Ok(())); } fn t4() { hook_start(); - match (&1, &1) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_eq(1, 1); hook_end(); } fn abs(x: i32) -> i32 { hook_start(); if x >= 0 { - { - ::std::io::_print(format_args!("x is positive\n")); - }; + log("x is positive"); x } else { - { - ::std::io::_print(format_args!("x is negative\n")); - }; + log("x is negative"); -x } } fn abs2(x: i32) -> i32 { hook_end(); if x >= 0 { - { - ::std::io::_print(format_args!("x is positive\n")); - }; + log("x is positive"); x } else { - { - ::std::io::_print(format_args!("x is negative\n")); - }; + log("x is negative"); -x } } diff --git a/cvlr-hook/tests/expand/test_hook_combined.rs b/cvlr-hook/tests/expand/test_hook_combined.rs index e0a3bc7..41aead5 100644 --- a/cvlr-hook/tests/expand/test_hook_combined.rs +++ b/cvlr-hook/tests/expand/test_hook_combined.rs @@ -8,6 +8,20 @@ fn hook_end() { (); } +// plain functions instead of assert_eq!/println! so the expanded output +// does not depend on the compiler's builtin macro lowering, which +// changes between rustc versions +fn check_eq(_a: i32, _b: i32) { + (); +} + +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} + +fn log(_msg: &str) { + (); +} #[cvlr_hook_on_entry(hook_start())] #[cvlr_hook_on_exit(hook_end())] @@ -18,37 +32,37 @@ fn tmp() -> Result<()> { } fn t3() { - assert_eq!(tmp(), Ok(())); + check_res(tmp(), Ok(())); } #[cvlr_hook_on_entry(hook_start())] #[cvlr_hook_on_exit(hook_end())] fn t4() { // hook start inserted here - assert_eq!(1, 1); + check_eq(1, 1); // hook end inserted here } #[cvlr_hook_on_entry(hook_start())] fn abs(x : i32) -> i32 { // hook start inserted here - if x >= 0 { - println!("x is positive"); - x - } else { - println!("x is negative"); - -x + if x >= 0 { + log("x is positive"); + x + } else { + log("x is negative"); + -x } } #[cvlr_hook_on_exit(hook_end())] fn abs2(x : i32) -> i32 { // hook end inserted here - if x >= 0 { - println!("x is positive"); - x - } else { - println!("x is negative"); - -x + if x >= 0 { + log("x is positive"); + x + } else { + log("x is negative"); + -x } -} \ No newline at end of file +} diff --git a/cvlr-hook/tests/expand/test_hook_end.expanded.rs b/cvlr-hook/tests/expand/test_hook_end.expanded.rs index ee07c08..304434b 100644 --- a/cvlr-hook/tests/expand/test_hook_end.expanded.rs +++ b/cvlr-hook/tests/expand/test_hook_end.expanded.rs @@ -2,49 +2,19 @@ use cvlr_hook::cvlr_hook_on_exit; fn hook() { (); } +fn check_eq(_a: i32, _b: i32) { + (); +} +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} fn t1() { - match (&1, &1) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; - match (&2, &2) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_eq(1, 1); + check_eq(2, 2); hook(); } fn t2() { - match (&1, &1) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_eq(1, 1); hook(); } fn tmp() -> Result<()> { @@ -52,17 +22,5 @@ fn tmp() -> Result<()> { Ok(()) } fn t3() { - match (&tmp(), &Ok(())) { - (left_val, right_val) => { - if !(*left_val == *right_val) { - let kind = ::core::panicking::AssertKind::Eq; - ::core::panicking::assert_failed( - kind, - &*left_val, - &*right_val, - ::core::option::Option::None, - ); - } - } - }; + check_res(tmp(), Ok(())); } diff --git a/cvlr-hook/tests/expand/test_hook_end.rs b/cvlr-hook/tests/expand/test_hook_end.rs index 715701f..15824b8 100644 --- a/cvlr-hook/tests/expand/test_hook_end.rs +++ b/cvlr-hook/tests/expand/test_hook_end.rs @@ -4,17 +4,28 @@ fn hook() { (); } +// plain functions instead of assert_eq! so the expanded output does not +// depend on the compiler's builtin macro lowering, which changes +// between rustc versions +fn check_eq(_a: i32, _b: i32) { + (); +} + +fn check_res(_a: Result<()>, _b: Result<()>) { + (); +} + #[cvlr_hook_on_exit(hook())] fn t1() { - assert_eq!(1, 1); + check_eq(1, 1); // hook inserted here - assert_eq!(2, 2); + check_eq(2, 2); } #[cvlr_hook_on_exit(hook())] fn t2() { // hook inserted here - assert_eq!(1, 1); + check_eq(1, 1); } #[cvlr_hook_on_exit(hook())] @@ -24,5 +35,5 @@ fn tmp() -> Result<()> { } fn t3() { - assert_eq!(tmp(), Ok(())); -} \ No newline at end of file + check_res(tmp(), Ok(())); +} diff --git a/cvlr-hook/tests/expand/test_hook_start.expanded.rs b/cvlr-hook/tests/expand/test_hook_start.expanded.rs index e3b6c5f..404f684 100644 --- a/cvlr-hook/tests/expand/test_hook_start.expanded.rs +++ b/cvlr-hook/tests/expand/test_hook_start.expanded.rs @@ -2,9 +2,10 @@ use cvlr_hook::cvlr_hook_on_entry; fn hook() { (); } +fn work(_msg: &str) { + (); +} fn t1() { hook(); - { - ::std::io::_print(format_args!("t1\n")); - }; + work("t1"); } diff --git a/cvlr-hook/tests/expand/test_hook_start.rs b/cvlr-hook/tests/expand/test_hook_start.rs index 2ad2b03..3e34e5c 100644 --- a/cvlr-hook/tests/expand/test_hook_start.rs +++ b/cvlr-hook/tests/expand/test_hook_start.rs @@ -4,8 +4,15 @@ fn hook() { (); } +// plain function instead of println! so the expanded output does not +// depend on the compiler's builtin macro lowering, which changes +// between rustc versions +fn work(_msg: &str) { + (); +} + #[cvlr_hook_on_entry(hook())] fn t1() { // hook inserted here - println!("t1"); -} \ No newline at end of file + work("t1"); +} From ba64a821dd0f798707862d09b3e3a423203e47ef Mon Sep 17 00:00:00 2001 From: Chandrakana Nandi Date: Wed, 26 Aug 2026 15:24:26 -0700 Subject: [PATCH 11/13] undo previous yml change --- .github/workflows/main.yml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 5164e9d..8f237ec 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -43,7 +43,5 @@ jobs: toolchain: stable - name: Install cargo-expand run: cargo install cargo-expand - - name: Run cargo test (excluding cvlr-hook) - run: cargo test --verbose --workspace --exclude cvlr-hook - - name: Run cvlr-hook tests serially - run: cargo test -p cvlr-hook --test tests -- --test-threads=1 + - name: Run cargo test + run: cargo test --verbose From 712c1aee3a2fdf4da17811ad6f88a365209397c2 Mon Sep 17 00:00:00 2001 From: Julian Date: Thu, 27 Aug 2026 07:59:50 -0400 Subject: [PATCH 12/13] bump version to 0.6.2 to reflect changes for cvlr-soroban --- Cargo.lock | 24 ++++++++++++------------ Cargo.toml | 26 +++++++++++++------------- 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 539bb7d..f2a7cd3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,7 +4,7 @@ version = 4 [[package]] name = "cvlr" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr-asserts", "cvlr-decimal", @@ -21,7 +21,7 @@ dependencies = [ [[package]] name = "cvlr-asserts" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "cvlr-asserts", @@ -30,7 +30,7 @@ dependencies = [ [[package]] name = "cvlr-decimal" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "cvlr-asserts", @@ -41,7 +41,7 @@ dependencies = [ [[package]] name = "cvlr-derive" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "macrotest", @@ -53,7 +53,7 @@ dependencies = [ [[package]] name = "cvlr-early-panic" -version = "0.6.1" +version = "0.6.2" dependencies = [ "macrotest", "proc-macro2", @@ -64,7 +64,7 @@ dependencies = [ [[package]] name = "cvlr-fixed" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr-asserts", "cvlr-log", @@ -74,7 +74,7 @@ dependencies = [ [[package]] name = "cvlr-hook" -version = "0.6.1" +version = "0.6.2" dependencies = [ "macrotest", "quote", @@ -84,7 +84,7 @@ dependencies = [ [[package]] name = "cvlr-log" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "cvlr-mathint", @@ -94,7 +94,7 @@ dependencies = [ [[package]] name = "cvlr-macros" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "darling", @@ -107,7 +107,7 @@ dependencies = [ [[package]] name = "cvlr-mathint" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "cvlr-asserts", @@ -116,14 +116,14 @@ dependencies = [ [[package]] name = "cvlr-nondet" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr-asserts", ] [[package]] name = "cvlr-spec" -version = "0.6.1" +version = "0.6.2" dependencies = [ "cvlr", "cvlr-asserts", diff --git a/Cargo.toml b/Cargo.toml index aadb351..f9f20ec 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -16,7 +16,7 @@ members = [ ] [workspace.package] -version = "0.6.1" +version = "0.6.2" authors = [ "Arie Gurfinkel ", "Jorge A. Navas ", @@ -51,15 +51,15 @@ syn = "2" macrotest = "1" trybuild = "1" -cvlr = { path = "cvlr", version = "=0.6.1" } -cvlr-asserts = { path = "cvlr-asserts", version = "=0.6.1" } -cvlr-mathint = { path = "cvlr-mathint", version = "=0.6.1" } -cvlr-nondet = { path = "cvlr-nondet", default-features = false, version = "=0.6.1" } -cvlr-log = { path = "cvlr-log", version = "=0.6.1" } -cvlr-macros = { path = "cvlr-macros", version = "=0.6.1" } -cvlr-early-panic = { path = "cvlr-early-panic", version = "=0.6.1" } -cvlr-hook = { path = "cvlr-hook", version = "=0.6.1" } -cvlr-fixed = { path = "cvlr-fixed", version = "=0.6.1" } -cvlr-decimal = { path = "cvlr-decimal", version = "=0.6.1" } -cvlr-derive = { path = "cvlr-derive", version = "=0.6.1" } -cvlr-spec = { path = "cvlr-spec", version = "=0.6.1" } +cvlr = { path = "cvlr", version = "=0.6.2" } +cvlr-asserts = { path = "cvlr-asserts", version = "=0.6.2" } +cvlr-mathint = { path = "cvlr-mathint", version = "=0.6.2" } +cvlr-nondet = { path = "cvlr-nondet", default-features = false, version = "=0.6.2" } +cvlr-log = { path = "cvlr-log", version = "=0.6.2" } +cvlr-macros = { path = "cvlr-macros", version = "=0.6.2" } +cvlr-early-panic = { path = "cvlr-early-panic", version = "=0.6.2" } +cvlr-hook = { path = "cvlr-hook", version = "=0.6.2" } +cvlr-fixed = { path = "cvlr-fixed", version = "=0.6.2" } +cvlr-decimal = { path = "cvlr-decimal", version = "=0.6.2" } +cvlr-derive = { path = "cvlr-derive", version = "=0.6.2" } +cvlr-spec = { path = "cvlr-spec", version = "=0.6.2" } From 39316e301b3f06b8f056a9a778b2880ea5d23eaa Mon Sep 17 00:00:00 2001 From: Julian Date: Thu, 27 Aug 2026 10:00:17 -0400 Subject: [PATCH 13/13] revert change from env to cvlr --- Cargo.lock | 24 ++++++++++++------------ Cargo.toml | 26 +++++++++++++------------- cvlr-asserts/src/core.rs | 2 +- cvlr-asserts/src/log.rs | 2 +- cvlr-log/src/core.rs | 2 +- cvlr-mathint/src/nativeint_u64.rs | 2 +- cvlr-nondet/src/scalars.rs | 2 +- cvlr/src/u128_arith.rs | 2 +- 8 files changed, 31 insertions(+), 31 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index f2a7cd3..539bb7d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,7 +4,7 @@ version = 4 [[package]] name = "cvlr" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr-asserts", "cvlr-decimal", @@ -21,7 +21,7 @@ dependencies = [ [[package]] name = "cvlr-asserts" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "cvlr-asserts", @@ -30,7 +30,7 @@ dependencies = [ [[package]] name = "cvlr-decimal" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "cvlr-asserts", @@ -41,7 +41,7 @@ dependencies = [ [[package]] name = "cvlr-derive" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "macrotest", @@ -53,7 +53,7 @@ dependencies = [ [[package]] name = "cvlr-early-panic" -version = "0.6.2" +version = "0.6.1" dependencies = [ "macrotest", "proc-macro2", @@ -64,7 +64,7 @@ dependencies = [ [[package]] name = "cvlr-fixed" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr-asserts", "cvlr-log", @@ -74,7 +74,7 @@ dependencies = [ [[package]] name = "cvlr-hook" -version = "0.6.2" +version = "0.6.1" dependencies = [ "macrotest", "quote", @@ -84,7 +84,7 @@ dependencies = [ [[package]] name = "cvlr-log" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "cvlr-mathint", @@ -94,7 +94,7 @@ dependencies = [ [[package]] name = "cvlr-macros" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "darling", @@ -107,7 +107,7 @@ dependencies = [ [[package]] name = "cvlr-mathint" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "cvlr-asserts", @@ -116,14 +116,14 @@ dependencies = [ [[package]] name = "cvlr-nondet" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr-asserts", ] [[package]] name = "cvlr-spec" -version = "0.6.2" +version = "0.6.1" dependencies = [ "cvlr", "cvlr-asserts", diff --git a/Cargo.toml b/Cargo.toml index f9f20ec..aadb351 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -16,7 +16,7 @@ members = [ ] [workspace.package] -version = "0.6.2" +version = "0.6.1" authors = [ "Arie Gurfinkel ", "Jorge A. Navas ", @@ -51,15 +51,15 @@ syn = "2" macrotest = "1" trybuild = "1" -cvlr = { path = "cvlr", version = "=0.6.2" } -cvlr-asserts = { path = "cvlr-asserts", version = "=0.6.2" } -cvlr-mathint = { path = "cvlr-mathint", version = "=0.6.2" } -cvlr-nondet = { path = "cvlr-nondet", default-features = false, version = "=0.6.2" } -cvlr-log = { path = "cvlr-log", version = "=0.6.2" } -cvlr-macros = { path = "cvlr-macros", version = "=0.6.2" } -cvlr-early-panic = { path = "cvlr-early-panic", version = "=0.6.2" } -cvlr-hook = { path = "cvlr-hook", version = "=0.6.2" } -cvlr-fixed = { path = "cvlr-fixed", version = "=0.6.2" } -cvlr-decimal = { path = "cvlr-decimal", version = "=0.6.2" } -cvlr-derive = { path = "cvlr-derive", version = "=0.6.2" } -cvlr-spec = { path = "cvlr-spec", version = "=0.6.2" } +cvlr = { path = "cvlr", version = "=0.6.1" } +cvlr-asserts = { path = "cvlr-asserts", version = "=0.6.1" } +cvlr-mathint = { path = "cvlr-mathint", version = "=0.6.1" } +cvlr-nondet = { path = "cvlr-nondet", default-features = false, version = "=0.6.1" } +cvlr-log = { path = "cvlr-log", version = "=0.6.1" } +cvlr-macros = { path = "cvlr-macros", version = "=0.6.1" } +cvlr-early-panic = { path = "cvlr-early-panic", version = "=0.6.1" } +cvlr-hook = { path = "cvlr-hook", version = "=0.6.1" } +cvlr-fixed = { path = "cvlr-fixed", version = "=0.6.1" } +cvlr-decimal = { path = "cvlr-decimal", version = "=0.6.1" } +cvlr-derive = { path = "cvlr-derive", version = "=0.6.1" } +cvlr-spec = { path = "cvlr-spec", version = "=0.6.1" } diff --git a/cvlr-asserts/src/core.rs b/cvlr-asserts/src/core.rs index 22f95df..6768e3b 100644 --- a/cvlr-asserts/src/core.rs +++ b/cvlr-asserts/src/core.rs @@ -1,7 +1,7 @@ mod rt_decls { #[cfg_attr( all(target_family = "wasm", target_os = "none"), - link(wasm_import_module = "cvlr") + link(wasm_import_module = "env") )] extern "C" { pub fn CVT_assume(_c: bool); diff --git a/cvlr-asserts/src/log.rs b/cvlr-asserts/src/log.rs index 036aeab..e1d0e96 100644 --- a/cvlr-asserts/src/log.rs +++ b/cvlr-asserts/src/log.rs @@ -1,7 +1,7 @@ mod rt_decls { #[cfg_attr( all(target_family = "wasm", target_os = "none"), - link(wasm_import_module = "cvlr") + link(wasm_import_module = "env") )] extern "C" { #![allow(improper_ctypes)] diff --git a/cvlr-log/src/core.rs b/cvlr-log/src/core.rs index 09f0e4a..cd9da63 100644 --- a/cvlr-log/src/core.rs +++ b/cvlr-log/src/core.rs @@ -1,7 +1,7 @@ pub mod rt_decls { #[cfg_attr( all(target_family = "wasm", target_os = "none"), - link(wasm_import_module = "cvlr") + link(wasm_import_module = "env") )] #[allow(improper_ctypes)] extern "C" { diff --git a/cvlr-mathint/src/nativeint_u64.rs b/cvlr-mathint/src/nativeint_u64.rs index 248e168..61dff4b 100644 --- a/cvlr-mathint/src/nativeint_u64.rs +++ b/cvlr-mathint/src/nativeint_u64.rs @@ -14,7 +14,7 @@ mod rt_decls { #[cfg_attr( all(target_family = "wasm", target_os = "none"), - link(wasm_import_module = "cvlr") + link(wasm_import_module = "env") )] extern "C" { pub fn CVT_nativeint_u64_eq(_: u64, _: u64) -> BoolU64; diff --git a/cvlr-nondet/src/scalars.rs b/cvlr-nondet/src/scalars.rs index ed6d901..a435621 100644 --- a/cvlr-nondet/src/scalars.rs +++ b/cvlr-nondet/src/scalars.rs @@ -3,7 +3,7 @@ use crate::Nondet; mod rt_decls { #[cfg_attr( all(target_family = "wasm", target_os = "none"), - link(wasm_import_module = "cvlr") + link(wasm_import_module = "env") )] #[allow(improper_ctypes)] extern "C" { diff --git a/cvlr/src/u128_arith.rs b/cvlr/src/u128_arith.rs index 45c267f..5331da0 100644 --- a/cvlr/src/u128_arith.rs +++ b/cvlr/src/u128_arith.rs @@ -1,7 +1,7 @@ mod rt_decls { #[cfg_attr( all(target_family = "wasm", target_os = "none"), - link(wasm_import_module = "cvlr") + link(wasm_import_module = "env") )] #[allow(improper_ctypes)] extern "C" {