fix(hax-lib): add non-computable assert_prop

hax-lib/proofs/fstar/extraction/Hax_lib.fst

@@ -2,8 +2,11 @@ module Hax_lib
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open FStar.Tactics
 
-val v_assert (p: Type0) : Pure unit (requires p) (ensures (fun x -> p))
-let v_assert (v__formula: Type0) = ()
+val v_assert (p: bool) : Pure unit (requires p) (ensures (fun x -> p))
+let v_assert (v__formula: bool) = ()
+
+val assert_prop (p: Type0) : Pure unit (requires p) (ensures (fun x -> p))
+let assert_prop (v__formula: Type0) = ()
 
 val v_assume (p: Type0) : Pure unit (requires True) (ensures (fun x -> p))
 let v_assume (v__formula: Type0) = assume v__formula

hax-lib/src/implementation.rs

@@ -54,7 +54,7 @@ macro_rules! debug_assert {
 /// into a `assert` in the backend.
 macro_rules! assert {
     ($($arg:tt)*) => {
-        $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $(::hax_lib::Prop::from($arg))*)
+        $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $($arg)*)
     };
 }
 
@@ -63,7 +63,28 @@ macro_rules! assert {
 /// This function exists only when compiled with `hax`, and is not
 /// meant to be used directly. It is called by `assert!` only in
 /// appropriate situations.
-pub fn assert(_formula: Prop) {}
+pub fn assert(_formula: bool) {}
+
+#[macro_export]
+/// Assert a logical proposition [`Prop`]: this exists only in the backends of
+/// hax. In Rust, this macro expands to an empty block `{ }`.
+macro_rules! assert_prop {
+    ($($arg:tt)*) => {
+        {
+            #[cfg(hax)]
+            {
+                $crate::assert_prop($crate::Prop::from($($arg)*));
+            }
+        }
+    };
+}
+
+#[doc(hidden)]
+#[cfg(hax)]
+/// This function exists only when compiled with `hax`, and is not meant to be
+/// used directly. It is called by `assert_prop!` only in appropriate
+/// situations.
+pub fn assert_prop(_formula: Prop) {}
 
 #[doc(hidden)]
 #[cfg(hax)]

hax-lib/src/lib.rs

@@ -5,10 +5,12 @@
 //! # Example:
 //!
 //! ```rust
+//! use hax_lib::*;
 //! fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
 //!   hax_lib::assume!(x.len() == y.len());
-//!   hax_lib::assert!(hax_lib::forall(|i: usize| hax_lib::implies(i < x.len(), || x[i] < 4242)));
-//!   hax_lib::debug_assert!(hax_lib::exists(|i: usize| hax_lib::implies(i < x.len(), || x[i] > 123)));
+//!   hax_lib::assert!(x.len() >= 0);
+//!   hax_lib::assert_prop!(forall(|i: usize| implies(i < x.len(), x[i] < 4242)));
+//!   hax_lib::debug_assert!(exists(|i: usize| implies(i < x.len(), x[i] > 123)));
 //!   x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
 //! }
 //! ```