Skip to content

Julian/soroban auto sanity #48

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
julian-certora merged 16 commits into from
Aug 27, 2026
Merged

Julian/soroban auto sanity #48

Show file tree
Hide file tree
Changes from 15 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
b7072c5
work toward generating sanity rules for soroban and compiling it
julian-certora Aug 14, 2026
85fef5f
export some primitives for use in cvlr_soroban
julian-certora Aug 25, 2026
4392f0f
Merge branch 'main' into julian/soroban_auto_sanity
julian-certora Aug 26, 2026
34e159d
clean up 'env'
julian-certora Aug 26, 2026
e187d3a
Merge branch 'julian/soroban_auto_sanity' of github.com:Certora/cvlr …
julian-certora Aug 26, 2026
a579210
remove duplicate annotation
julian-certora Aug 26, 2026
fc92ab0
fmt
julian-certora Aug 26, 2026
ea27c3a
remove default-features=false
julian-certora Aug 26, 2026
c4891c1
trying to fix CI based on copilot advice
chandrakananandi Aug 26, 2026
deb969f
forgot to exclude hook tests from all tests
chandrakananandi Aug 26, 2026
428ce77
add workspace
chandrakananandi Aug 26, 2026
d55fd8b
avoid builtin macros that affect expansion across rustc versions
chandrakananandi Aug 26, 2026
ba64a82
undo previous yml change
chandrakananandi Aug 26, 2026
712c1ae
bump version to 0.6.2 to reflect changes for cvlr-soroban
julian-certora Aug 27, 2026
ec25cc9
Merge branch 'julian/soroban_auto_sanity' of github.com:Certora/cvlr …
julian-certora Aug 27, 2026
39316e3
revert change from env to cvlr
julian-certora Aug 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

26 changes: 13 additions & 13 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ members = [
]

[workspace.package]
version = "0.6.1"
version = "0.6.2"

@1arie1 1arie1 Aug 27, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do not manually update the version. the version is updated automatically as part of cargo-release

@julian-certora julian-certora Aug 27, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thanks. reverted.

authors = [
"Arie Gurfinkel <arie@certora.com>",
"Jorge A. Navas <jorge@certora.com>",
Expand Down Expand Up @@ -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" }
4 changes: 4 additions & 0 deletions cvlr-asserts/src/core.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,8 @@
mod rt_decls {
#[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);
Expand Down
4 changes: 4 additions & 0 deletions cvlr-asserts/src/log.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,8 @@
mod rt_decls {
#[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
Expand Down
53 changes: 15 additions & 38 deletions cvlr-hook/tests/expand/test_hook_combined.expanded.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}
44 changes: 29 additions & 15 deletions cvlr-hook/tests/expand/test_hook_combined.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())]
Expand All @@ -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
}
}
}
62 changes: 10 additions & 52 deletions cvlr-hook/tests/expand/test_hook_end.expanded.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,67 +2,25 @@ 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<()> {
hook();
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(()));
}
Loading
Loading