Steel: issue with normalization and fst/snd

[cmovcc]

Hi, I noticed the following 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_fst

open Steel.FractionalPermission
module Mem = Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference

#set-options "--ide_id_info_off"

assume
val linked_tree (#a: Type0) (ptr: ref a)
  : Tot vprop

[@@ expect_failure]
let rec f1 #a (ptr: ref a) (n: nat)
  : SteelT (ref a & nat)
  (linked_tree ptr) (fun r -> linked_tree (fst r))
  =
  if n = 0 then return #(ref a & nat) (ptr, 0)
  else
    let a, b = f1 ptr (n - 1) in
    a, 0

[@@ expect_failure]
let rec f2 #a (ptr: ref a) (n: nat)
  : SteelT (ref a & nat)
  (linked_tree ptr) (fun (ptr', _) -> linked_tree ptr')
  =
  if n = 0 then return #(ref a & nat) (ptr, 0)
  else
    let r = f2 ptr (n - 1) in
    fst r, 0

let rec f3 #a (ptr: ref a) (n: nat)
  : SteelT (ref a & nat)
  (linked_tree ptr) (fun r -> linked_tree (fst r))
  =
  if n = 0 then return #(ref a & nat) (ptr, 0)
  else
    let r = f3 ptr (n - 1) in
    fst r, 0

[@@expect_failure]
let f4 #a (ptr: ref a) (n: nat)
  : SteelT (ref a)
  (linked_tree ptr) (fun r -> linked_tree r)
  =
  let a, b = f3 ptr n in
  return a

let f5 #a (ptr: ref a) (n: nat)
  : SteelT (ref a)
  (linked_tree ptr) (fun r -> linked_tree r)
  =
  let r = f3 ptr n in
  return (fst r)

While manipulating Steel functions returning several objects including some required to respect the separating propositions, this lead to programs that are less readable, and it seems to make the verification quite painful with more complicated examples. CCing @R1kM. Thanks a lot in advance!