Steel: issue with subcomp framing rule for return?

[cmovcc]

Hi, I noticed the following small bug while using Steel with selectors, that also affects Steel without selectors. It can be demonstrated with the following minimal example using a dummy structure without selectors.

module Bug_subcomp_return

open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference

assume
val linked_tree (#a: Type) (ptr: ref a) : vprop

[@@expect_failure]
let f1 (#a: Type) (ptr: ref a) : SteelT (ref a)
  (linked_tree ptr) (fun ptr' -> linked_tree ptr')
  =
  return ptr

let f2 (#a: Type) (ptr: ref a) : SteelT (ref a)
  (linked_tree ptr) (fun ptr' -> linked_tree ptr')
  =
  ();
  return ptr

Seems like a variation of #2369. CCing @R1kM . Thanks a lot in advance!

[aseemr]

@R1kM, any ideas what's happening here?

[R1kM]

I didn't get a chance to look yet, I'll try to inspect the queries and report back.

[aseemr]

Now I remember, I also have seen this kind of thing. Whenever the post assertion depends on the return value, I usually bind the return value explicitly, and then it works. E.g. using Steel.ST:

let f1 (#a: Type) (ptr: ref a) : STT (ref a)
  (linked_tree ptr) (fun ptr' -> linked_tree ptr')
  = let res = ptr in
    return res

works, but this doesn't:

let f1 (#a: Type) (ptr: ref a) : STT (ref a)
  (linked_tree ptr) (fun ptr' -> linked_tree ptr')
  = return ptr

Also the failure does not seem to be in SMT. The error that I get is:

(Error) user tactic failed: `could not find a solution for unifying
Test.linked_tree ptr7991
and
Test.linked_tree x10264`

(with --print_full_names option on).

[R1kM]

Yes, we observed something similar. In @cmovcc's initial usecase, this was occuring when if/then/else branches consisted of a single return, he minimized it further to this small snippet.