val rec_perm (r: rec2) (v: rec_repr) : vprop
val rec_perm (r: rec2) (v: rec_repr) : vprop
let rec_perm (r:rec2) (v:rec_repr)
  : vprop
  = R.pts_to r.r1 v.v1 **
    R.pts_to r.r2 v.v2
(*
   Copyright 2023 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Records
open Pulse.Lib.Pervasives
module R = Pulse.Lib.Reference
module U8 = FStar.UInt8

(* test record mutation and permissions for records of byte refs *)

noeq
type rec2 = {
  r1: R.ref U8.t;
  r2: R.ref U8.t;
}

type rec_repr = {
  v1: U8.t;
  v2: U8.t;
}
/
Pulse.Lib.Reference.fsti.checked Pulse.Lib.Pervasives.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked
Records.fst
r: Records.rec2 -> v: Records.rec_repr -> Pulse.Lib.Core.vprop
Records.rec2 Records.rec_repr Pulse.Lib.Core.op_Star_Star Pulse.Lib.Reference.pts_to FStar.UInt8.t Records.__proj__Mkrec2__item__r1 PulseCore.FractionalPermission.full_perm Records.__proj__Mkrec_repr__item__v1 Records.__proj__Mkrec2__item__r2 Records.__proj__Mkrec_repr__item__v2 Pulse.Lib.Core.vprop
let rec_perm (r: rec2) (v: rec_repr) : vprop =
  
R.pts_to r.r1 v.v1 ** R.pts_to r.r2 v.v2