Records with references are tedious to work with

[nikswamy]

Syntactically, p.a := v does not parse. You have to write (write p.a v) instead.

But, more significantly, you need explicit rewrites to unpack the permissions in a record and then pack it back at the end. We should automate this.

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/RecordWithRefs.fst

[nikswamy]

• The parser is fixed to allow p.a := v

• The unfold and fold features help significantly with unpacking and packing records.

Unfold & Fold

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));
    ()
}

Fold and Unfold, with binders

You can also combine binding witnesses with fold and unfold, like this

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);
    ()
}

On the fold side, this is a bit subtle, since in addition to folding the head symbol u8_pair_pred you also have to fold fst and snd

Folding with a ghost function

The style that we're settling on for folding is to use a ghost function to package things up.

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
}

[nikswamy]

There are still two remaining problems:

1. Allocating a record of references

Currently, you have to do this:

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
}

where fold_rec_perm is

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))
}

You need to explicitly do the two rewrites to "rename" r1 as r.r1 and r2 as r.r2 and then call the fold_rec_perm lemma. Is there a way to automate this?

[nikswamy]

2. Record syntax doesn't work in Pulse

E.g., writing ...

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

Causes a crash with

(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)

[nikswamy]

Slightly more compact syntax for rewrites allows us to write this now:

fn alloc_rec_alt (v1 v2:U8.t)
  requires emp
  returns r:rec2
  ensures rec_perm r (mk_rec_repr v1 v2)
{
  let r1 = alloc v1;
  let r2 = alloc v2; 
  let r = mk_rec2 r1 r2;
  rewrite each r1 as r.r1, r2 as r.r2;
  fold_rec_perm r;
  r
}

[nikswamy]

record literal syntax is fixed since 5e397ba