From 3970bb3f5028fd6208c9be3905b98032c6b21915 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Thu, 20 Feb 2025 14:31:46 +0100
Subject: [PATCH] test(hax-lib): `<BACKEND>_replace_body`

---
 .../toolchain__attributes into-fstar.snap     | 20 +++++++++++++++++++
 tests/attributes/src/lib.rs                   | 18 +++++++++++++++++
 2 files changed, 38 insertions(+)

diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index aefd0338d..9b5572b39 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/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"
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 589472bed..7fc013810 100644
--- a/tests/attributes/src/lib.rs
+++ b/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::*;