Merge pull request #1351 from cryspen/fixes-assume

fix(hax-lib/assume): fixes assume and assert_prop

Author: maximebuyse

engine/lib/phases/phase_specialize.ml

@@ -291,6 +291,25 @@ module Make (F : Features.T) =
 
       module Attrs = Attr_payloads.Make (F) (Error)
 
+      (** Drop `from` or `into` when they are of type `T -> T`, for any `T`. *)
+      let remove_from_into_identity =
+        object
+          inherit [_] Visitors.map as super
+
+          method! visit_expr () e =
+            let e =
+              match e.e with
+              | App { f = { e = GlobalVar f; _ }; args = [ x ]; _ }
+                when [%equal: ty] e.typ x.typ
+                     && (Ast.Global_ident.eq_name Core__convert__Into__into f
+                        || Ast.Global_ident.eq_name Core__convert__From__from f
+                        ) ->
+                  x
+              | _ -> e
+            in
+            super#visit_expr () e
+        end
+
       let visitor =
         object (self)
           inherit [_] Visitors.map as super
@@ -354,5 +373,7 @@ module Make (F : Features.T) =
         end
 
       let ditems (l : A.item list) : B.item list =
-        List.map ~f:(visitor#visit_item ()) l
+        List.map
+          ~f:(visitor#visit_item () >> remove_from_into_identity#visit_item ())
+          l
     end)

hax-lib/macros/src/implementation.rs

@@ -817,37 +817,41 @@ macro_rules! make_quoting_proc_macro {
             #[proc_macro]
             pub fn [<$backend _expr>](payload: pm::TokenStream) -> pm::TokenStream {
                 let ts: TokenStream = quote::expression(quote::InlineExprType::Unit, payload).into();
-                quote!{
+                quote!{{
                     #[cfg([< hax_backend_ $backend >])]
                     {
                         #ts
                     }
-                }.into()
+                }}.into()
             }
 
             #[doc = concat!("The `Prop` version of `", stringify!($backend), "_expr`.")]
             #[proc_macro]
             pub fn [<$backend _prop_expr>](payload: pm::TokenStream) -> pm::TokenStream {
                 let ts: TokenStream = quote::expression(quote::InlineExprType::Prop, payload).into();
-                quote!{
+                quote!{{
                     #[cfg([< hax_backend_ $backend >])]
                     {
                         #ts
                     }
-                }.into()
+                    #[cfg(not([< hax_backend_ $backend >]))]
+                    {
+                        ::hax_lib::Prop::from_bool(true)
+                    }
+                }}.into()
             }
 
             #[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")]
             #[proc_macro]
             #[doc(hidden)]
             pub fn [<$backend _unsafe_expr>](payload: pm::TokenStream) -> pm::TokenStream {
                 let ts: TokenStream = quote::expression(quote::InlineExprType::Anything, payload).into();
-                quote!{
+                quote!{{
                     #[cfg([< hax_backend_ $backend >])]
                     {
                         #ts
                     }
-                }.into()
+                }}.into()
             }
 
             make_quoting_item_proc_macro!($backend, [< $backend _before >], ItemQuotePosition::Before, [< hax_backend_ $backend >]);

hax-lib/src/implementation.rs

@@ -73,7 +73,7 @@ macro_rules! assert_prop {
         {
             #[cfg(hax)]
             {
-                $crate::assert_prop($crate::Prop::from($($arg)*));
+                $crate::assert_prop(::hax_lib::Prop::from($($arg)*));
             }
         }
     };
@@ -97,7 +97,7 @@ pub fn assume(_formula: Prop) {}
 #[macro_export]
 macro_rules! assume {
     ($formula:expr) => {
-        $crate::assume(Prop::from($formula))
+        $crate::assume(::hax_lib::Prop::from($formula))
     };
 }
 

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -576,6 +576,12 @@ type t_Foo = {
   f_z:f_z: u32{b2t (((f_y +! f_x <: u32) +! f_z <: u32) >. mk_u32 3 <: bool)}
 }
 
+let props (_: Prims.unit) : Prims.unit =
+  let _:Prims.unit = Hax_lib.v_assume True in
+  let _:Prims.unit = Hax_lib.assert_prop True in
+  let _:Prims.unit = () in
+  ()
+
 let inlined_code__v_V: u8 = mk_u8 12
 
 let before_inlined_code = "example before"

tests/attributes/src/lib.rs

@@ -75,6 +75,11 @@ impl Foo {
     fn h(&self) {}
 }
 
+fn props() {
+    hax_lib::assume!(hax_lib::fstar::prop!("True"));
+    hax_lib::assert_prop!(hax_lib::fstar::prop!("True"));
+}
+
 #[hax::attributes]
 mod refined_arithmetic {
     use core::ops::{Add, Mul};