From 8dbfeeb1028e96998c007d2f6872f7bf5ccaefed Mon Sep 17 00:00:00 2001 From: Mihai Date: Sat, 13 Jun 2026 18:01:15 +0200 Subject: [PATCH 1/2] feat(cvlr-spec): add #![no_std] for wasm32v1-none / no_std consumers cvlr-spec uses only core (no std:: references), but lacks the #![no_std] attribute, so it pulls in std and fails to compile for downstream crates targeting wasm32v1-none (e.g. Soroban contracts on recent soroban-sdk). Adding the crate-level attribute makes it usable from no_std contexts; the crate already compiles unchanged otherwise. --- cvlr-spec/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/cvlr-spec/src/lib.rs b/cvlr-spec/src/lib.rs index 5af3123..2d535eb 100644 --- a/cvlr-spec/src/lib.rs +++ b/cvlr-spec/src/lib.rs @@ -1,3 +1,4 @@ +#![no_std] //! Specification language for CVL (Certora Verification Language) in Rust. //! //! This module provides a framework for writing specifications with preconditions From c648c2277c8b8c01965142d5c56709866d462898 Mon Sep 17 00:00:00 2001 From: Mihai Date: Sat, 27 Jun 2026 01:38:36 +0200 Subject: [PATCH 2/2] fix(cvlr-macros): make rule_for_spec snapshot toolchain-stable The macrotest snapshot recorded std's internal `vec!` desugaring (`<[_]>::into_vec(box_new([1, 2, 3]))`), which current stable expands to `box_assume_init_into_vec_unsafe(write_box_via_move(...))`. CI pins unpinned `stable`, so the byte-comparison drifts and fails on `main`. The fixture only needs a collection exposing `.len()` / `.iter().sum()`; swap `vec![1, 2, 3]` for the array `[1, 2, 3]`, which expands to itself and is immune to std-internal desugaring changes. Claude-Session: https://claude.ai/code/session_01VArXWJTqakNurd51jzwpHm --- cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs | 2 +- cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs index 1368e30..0b243d0 100644 --- a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs +++ b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs @@ -73,7 +73,7 @@ pub fn test_edge_cases() { } } pub fn test_spec_with_method_calls() { - let expr = <[_]>::into_vec(::alloc::boxed::box_new([1, 2, 3])); + let expr = [1, 2, 3]; { let _rule_name = "method_check"; let _spec = expr.len() > 0; diff --git a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs index a5649d9..baeef2e 100644 --- a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs +++ b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs @@ -115,7 +115,7 @@ pub fn test_edge_cases() { } pub fn test_spec_with_method_calls() { - let expr = vec![1, 2, 3]; + let expr = [1, 2, 3]; // Test with method calls in spec cvlr_rule_for_spec! {