[CN] Destroying and recreating an iterated Owned loses self-equality / Lemma backend should export range constraints for all SMT arrays

[dc-mak]

@septract shared this surprisingly interesting example of failed verification:

struct test_struct {
    int key_id[1];
};

void test_extract_noop (struct test_struct* c)
/*@
requires
    take Struct_in = Owned(c);
ensures
    take Struct_out = Owned(c);
    Struct_out == Struct_in;
@*/
{
    /*@ extract Owned<int>, 0u64; @*/
}

My best guess about this is the following:
Oh this ones a real doozy; here's what happened

1. Enter function
2. Explode struct - only left with Owned<int[1]>
3. Explode array - left with take A = each (..) { .. }
4. Use extract - left with Owned<int>, no empty each (..) { .. } because guard is empty
5. Exit function
6. Request struct
7. Request field of struct (Owned<int[1]>)
8. Request each (..) {..}
9. Move Owned<int> into a new take A2 = each (..) { .. }
10. Continue wrapping up resource
11. Now try to prove constraint, which involves two different arrays A1 == A2. Though this err doesn't produce one, the counter-example should be something out of range.
12. Cry because we're fundamentally dealing with finite maps and SMT maps are total/infinite.

The worst part about this is that even the usual approach of defining a (hypothetical Rocq provable) lemma for is not available to us because the it's the same resources used at two different times producing different SMT values, rather than two each resources defined over the same range.

This suggests (a) we need to be able to pass ghost arguments to lemmas (#540) and (b) the export from CN to Rocq should track and tag every ghost SMT value with its range to get around this.

Of course, even with a lemma, calling it here would be silly, so if possible, alternatives to the above proposal are welcome.