Julian/soroban auto sanity

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,4 +1,8 @@
 pub 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_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,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};
+pub use scalars::{
+    cvlr_nondet_small_i128, cvlr_nondet_small_u128, cvlr_nondet_u32, cvlr_nondet_u64,
+};

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