Julian/soroban auto sanity

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" }

cvlr-asserts/src/core.rs

@@ -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);

cvlr-asserts/src/log.rs

@@ -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

cvlr-log/src/core.rs

@@ -1,5 +1,9 @@
 pub mod rt_decls {
-    #[allow(improper_ctypes)]
+    #[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);
 

cvlr-mathint/src/nativeint_u64.rs

@@ -12,6 +12,10 @@ pub struct NativeIntU64(u64);
 mod rt_decls {
     type BoolU64 = u64;
 
+    #[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;

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};

cvlr-nondet/src/scalars.rs

@@ -1,6 +1,10 @@
 use crate::Nondet;
 
 mod rt_decls {
+    #[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

cvlr-spec/src/lib.rs

@@ -54,6 +54,7 @@
 //! // Define a simple spec - cvlr_true uses eval_with_states for ensures
 //! let spec = cvlr_spec(cvlr_true::<Counter>(), cvlr_true::<Counter>());
 //! ```
+#![no_std]
 
 mod combinators;
 mod formula;

cvlr/src/u128_arith.rs

@@ -1,4 +1,8 @@
 mod rt_decls {
+    #[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;