test(hax-lib): <BACKEND>_replace_body

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

@@ -381,6 +381,26 @@ let t_FieldElement = x: u16{x <=. mk_u16 2347}
 /// Example of a specific constraint on a value
 let t_CompressionFactor = x: u8{x =. mk_u8 4 || x =. mk_u8 5 || x =. mk_u8 10 || x =. mk_u8 11}
 '''
+"Attributes.Replace_body.fst" = '''
+module Attributes.Replace_body
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let f (x y: u8) : u8 = magic x
+
+type t_Foo = | Foo : t_Foo
+
+let impl_Foo__assoc_fn (self: t_Foo) (x: u8) : Prims.unit = (magic (self <: t_Foo)) x
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: Alloc.String.t_ToString t_Foo =
+  {
+    f_to_string_pre = (fun (self: t_Foo) -> true);
+    f_to_string_post = (fun (self: t_Foo) (out: Alloc.String.t_String) -> true);
+    f_to_string = fun (self: t_Foo) -> "The type was t_Foo"
+  }
+'''
 "Attributes.Requires_mut.fst" = '''
 module Attributes.Requires_mut
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/attributes/src/lib.rs

@@ -180,6 +180,24 @@ fn some_function() -> String {
     String::from("hello from Rust")
 }
 
+mod replace_body {
+    #[hax_lib::fstar::replace_body("magic ${x}")]
+    fn f(x: u8, y: u8) -> u8 {
+        1 + 2
+    }
+    struct Foo;
+    impl Foo {
+        #[hax_lib::fstar::replace_body("(magic (${self} <: $:{Self})) ${x}")]
+        fn assoc_fn(&self, x: u8) {}
+    }
+    impl ToString for Foo {
+        #[hax_lib::fstar::replace_body(r#""The type was $:{Self}""#)]
+        fn to_string(&self) -> String {
+            "Hello".into()
+        }
+    }
+}
+
 mod pre_post_on_traits_and_impls {
     use hax_lib::*;