feat(cvlr-spec): add #![no_std] for no_std / wasm32v1-none consumers

[mihaieremia]

Summary

cvlr-spec/src/lib.rs has no crate-level #![no_std] attribute, so the crate links std. Consumers that build under #![no_std] — e.g. Soroban smart contracts targeting wasm32v1-none, where the entire contract crate tree must be no_std — cannot depend on cvlr-spec as published without patching it.

This adds a single #![no_std] line to cvlr-spec. The crate compiles cleanly as no_std (no std-only items in use), so this is a non-breaking, additive change for existing std consumers (they continue to work via core/alloc).

+#![no_std]
 //! Specification language for CVL (Certora Verification Language) in Rust.

Motivation

We maintain the XOXNO rs-lending-xlm Stellar lending protocol and use CVLR for formal verification. To build the spec crates into our no_std Soroban contracts we currently vendor cvlr with exactly this one-line patch. Upstreaming it lets us (and other Soroban users) drop the vendor and consume cvlr directly.

Test plan

• Builds under no_std in our Certora pipeline (soroban-sdk 26.1, wasm32v1-none).
• Maintainer confirms it doesn't regress existing std consumers / CI.

Opening as draft for maintainer feedback on the approach.

[mihaieremia]

@1arie1 ping 🙏

[1arie1]

@mihaieremia some tests are failing after the change

[mihaieremia]

CI fix: the failing testing job is a pre-existing, unrelated macrotest snapshot drift

The red testing job (ubuntu + macos) is not caused by the #![no_std] change — it reproduces on main unchanged. Pushed a fix in c648c22.

Root cause

The failing test is cvlr-macros → test_assert_that::test_cvlr_assert_that_macro_expansion, a macrotest::expand snapshot test that byte-compares macro expansion against checked-in .expanded.rs files.

The only diverging fixture is test_cvlr_rule_for_spec, and the entire diff is one line — the source let expr = vec![1, 2, 3];. Std's internal vec! desugaring changed across toolchains:

	expansion of vec![1, 2, 3]
recorded snapshot	<[_]>::into_vec(::alloc::boxed::box_new([1, 2, 3]))
current stable (1.95.0)	::alloc::boxed::box_assume_init_into_vec_unsafe(::alloc::intrinsics::write_box_via_move(::alloc::boxed::Box::new_uninit(), [1, 2, 3]))

CI pins unpinned toolchain: stable, so it floats to the newest stable and no longer matches the snapshot recorded on an older one. Every line our macros generate (_rule_name / _spec / _base blocks) matches byte-for-byte — only std's vec! internals drifted.

Evidence it's pre-existing

• git diff main...HEAD (before the fix) touched only cvlr-spec/src/lib.rs.
• The cvlr-macros snapshot is byte-identical on main and this branch.
• Running the same test on a clean main worktree fails with the identical box_assume_init_into_vec_unsafe diff.
• macrotest reports 1 of 12 fixtures differ — only the one using vec!.

Fix

The fixture (test_spec_with_method_calls) only needs a collection exposing .len() / .iter().sum::<i32>(). Swapping vec![1, 2, 3] → [1, 2, 3] keeps the test's intent (method calls in a spec expression) and expands to itself, so the snapshot is immune to std-internal desugaring changes. Regenerating with MACROTEST=overwrite changed only that one snapshot line; the other 11 are untouched.

Full cargo test is green locally (Rust 1.95.0), including the trybuild compile test that compiles this fixture.

Happy to split this into its own PR if you'd prefer to keep the #![no_std] change isolated — it's just bundled here to get this PR's CI green, since main is currently red for the same reason.

[mihaieremia]

@1arie1 Fixed and all checks passed

[1arie1]

@mihaieremia thank you! merged.