Given the following rust function

#[refine_spec(where T: Foo, [requires(v > 0), requires(v < 10)])]
#[requires(v == 5)]
fn fun<T>(v: i32) -> i32 { ... }

I would imagine it would be expanded to something that looks like this:

#[refine_spec_id = "id0"]
fn fun_refine_spec_id0<T>() where T: Foo {}

#[refine_spec_id_ref = "id0"]
#[spec_id = "id1"]
fn fun_pre_item_id1<T>(v: i32) -> bool where T: Foo { v > 0 }

#[refine_spec_id_ref = "id0"]
#[spec_id = "id2"]
fn fun_pre_item_id2<T>(v: i32) -> bool where T: Foo { v < 10 }

#[spec_id = "id3"]
fn fun_pre_item_id3<T>(v: i32) -> bool { v == 5 }

#[pre_spec_id_ref = "id1"]
#[pre_spec_id_ref = "id2"]
#[pre_spec_id_ref = "id3"]
fn fun<T>(v: i32) -> i32 { ... }

And it would later be collected into a structure like so

pres: ["id3"]
posts: []
refined: ["id0" : {
    Pre(["id1", "id2"]), 
    Post([]),
}]

let f = closure! {
    requires(v > 0),
    requires(v < 10),
    ensures(result == v + 1),
    |v: i32| -> i32 { v + 1 }
};

let f = {
    struct ClosureId0<F>(F);
    
    impl<F> FnOnce<(i32,)> for ClosureId0<F>
      where F: FnOnce<(i32,)> -> i32
    {
        type Output = i32;
        extern "rust-call" fn call_once(self, args: (i32,)) -> i32 {
            self.0.call_once(args)
        }
    }
    impl<F> FnOnceSpec<(i32,)> for ClosureId0<F>
      where F: FnOnce<(i32,)> -> i32
    {
        #[pure]
        fn requires((v,): (i32,)) -> bool {
            (v > 0) && (v < 10)
        }
        #[pure]
        fn ensures((v,): (i32,), result: i32) -> bool {
            (result == v + 1)
        }
    }
    ClosureId0(|v: i32| -> i32 { v + 1})
};