fn swap_pair_alt (p: u8_pair) (#v: erased u8_pair_repr)
  requires
    u8_pair_pred p v
  ensures
    u8_pair_pred p (snd v, fst v)
{
    unfold (u8_pair_pred p v);
    let x = !p.a;
    let y = !p.b;
    p.a := y;
    p.b := x;
    fold (u8_pair_pred p (snd v, fst v));
    ()
}

fn swap_pair_alt2 (p: u8_pair) (#v: erased u8_pair_repr)
  requires
    u8_pair_pred p v
  ensures
    u8_pair_pred p (snd v, fst v)
{

    with _p _v.
    unfold (u8_pair_pred _p _v);

    let x = !p.a;
    let y = !p.b;
    p.a := y;
    p.b := x;

    with _v1 _v2.
    fold [fst; snd] u8_pair_pred p (_v1, _v2);
    ()
}

ghost
fn fold_u8_pair_pred (x:u8_pair) (#u #v:erased U8.t)
  requires
    R.pts_to x.a full_perm u `star`
    R.pts_to x.b full_perm v
  ensures
    u8_pair_pred x (reveal u, reveal v)
{
   fold (u8_pair_pred x (reveal u, reveal v))
}

fn swap_pair_alt3 (p: u8_pair) (#v: erased u8_pair_repr)
  requires 
    u8_pair_pred p v
  ensures
    u8_pair_pred p (snd v, fst v)
{
    with _p _v.
    unfold (u8_pair_pred _p _v);
    
    let x = !p.a;
    let y = !p.b;
    p.a := y;
    p.b := x;
    
    fold_u8_pair_pred p
}

let mk_rec2 r1 r2 = { r1=r1; r2=r2 }

```pulse
fn alloc_rec (v1 v2:U8.t)
  requires emp
  returns r:rec2
  ensures rec_perm r (mk_rec_repr v1 v2)
{
  let r1 = alloc #U8.t v1;
  let r2 = alloc #U8.t v2; 
  let r = mk_rec2 r1 r2;
  (* Unfortunately, these two rewrites are still needed
     to "rename" r1 and r2 as r.r1 and r.r2 *)
  rewrite (R.pts_to r1 full_perm v1)
      as  (R.pts_to r.r1 full_perm v1);
  rewrite (R.pts_to r2 full_perm v2)
      as  (R.pts_to r.r2 full_perm v2);
  fold_rec_perm r;
  r
}

ghost
fn fold_rec_perm (r:rec2) (#v1 #v2:erased U8.t)
  requires
    R.pts_to r.r1 full_perm v1 **
    R.pts_to r.r2 full_perm v2
  ensures
    rec_perm r (mk_rec_repr v1 v2)
{
  fold (rec_perm r (mk_rec_repr v1 v2))
}

...
let r = {r1; r2};
...

(Error 17) Invalid_argument("List.combine: list lengths differ")
Records.fst(67,8-67,8): (Error 228) user tactic failed: `Pulse checker failed` (see also FStar.Tactics.V2.Derived.fst(447,4-449,16))
Records.fst(75,12-75,18): (Error) Ill-typed term: __dummy__ r1 r2
3 errors were reported (see above)