val preserved_split
  (#t: _) (#b: B.buffer t) (p: perm b)
  (from: U32.t)
  (mid: U32.t)
  (to: U32.t { U32.v from <= U32.v mid /\ U32.v mid <= U32.v to /\ U32.v to <= B.length b })
  (h h' : HS.mem)
: Lemma
  (preserved p from to h h' <==> (preserved p from mid h h' /\ preserved p mid to h h'))
let preserved_split p from mid to h h' =
  let s = B.deref h p in
  let s' = B.deref h' p in
  let prf () : Lemma
    (requires (valid_perm h p /\ valid_perm h' p))
    (ensures (preserved p from to h h' <==> (preserved p from mid h h' /\ preserved p mid to h h')))
  =
  assert (Seq.slice s' (U32.v from) (U32.v to) `Seq.equal` (Seq.slice s' (U32.v from) (U32.v mid) `Seq.append` Seq.slice s' (U32.v mid) (U32.v to)));
  assert (Seq.slice s (U32.v from) (U32.v to) `Seq.equal` (Seq.slice s (U32.v from) (U32.v mid) `Seq.append` Seq.slice s (U32.v mid) (U32.v to)));
  assert (Seq.slice s' (U32.v from) (U32.v mid) `Seq.equal` Seq.slice (Seq.slice s' (U32.v from) (U32.v to)) 0 (U32.v mid - U32.v from));
  assert (Seq.slice s' (U32.v mid) (U32.v to) `Seq.equal` Seq.slice (Seq.slice s' (U32.v from) (U32.v to)) (U32.v mid - U32.v from) (U32.v to - U32.v from))
  in
  Classical.move_requires prf ()
val preserved_split
  (#t: _) (#b: B.buffer t) (p: perm b)
  (from: U32.t)
  (mid: U32.t)
  (to: U32.t { U32.v from <= U32.v mid /\ U32.v mid <= U32.v to /\ U32.v to <= B.length b })
  (h h' : HS.mem)
: Lemma
  (preserved p from to h h' <==> (preserved p from mid h h' /\ preserved p mid to h h'))
let preserved_split p from mid to h h' =
let s = B.deref h p in
let s' = B.deref h' p in
let prf ()
    : Lemma (requires (valid_perm h p /\ valid_perm h' p))
      (ensures
        (preserved p from to h h' <==> (preserved p from mid h h' /\ preserved p mid to h h'))) =
  assert ((Seq.slice s' (U32.v from) (U32.v to))
      `Seq.equal`
      ((Seq.slice s' (U32.v from) (U32.v mid)) `Seq.append` (Seq.slice s' (U32.v mid) (U32.v to))));
  assert ((Seq.slice s (U32.v from) (U32.v to))
      `Seq.equal`
      ((Seq.slice s (U32.v from) (U32.v mid)) `Seq.append` (Seq.slice s (U32.v mid) (U32.v to))));
  assert ((Seq.slice s' (U32.v from) (U32.v mid))
      `Seq.equal`
      (Seq.slice (Seq.slice s' (U32.v from) (U32.v to)) 0 (U32.v mid - U32.v from)));
  assert ((Seq.slice s' (U32.v mid) (U32.v to))
      `Seq.equal`
      (Seq.slice (Seq.slice s' (U32.v from) (U32.v to))
          (U32.v mid - U32.v from)
          (U32.v to - U32.v from)))
in
Classical.move_requires prf ()
EverParse3d.Readable.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
EverParse3d.Readable.fst
LowStar.Buffer.buffer EverParse3d.Readable.perm FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder FStar.Monotonic.HyperStack.mem FStar.Classical.move_requires Prims.unit EverParse3d.Readable.valid_perm Prims.l_iff EverParse3d.Readable.preserved Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert FStar.Seq.Base.equal Prims.bool FStar.Seq.Base.slice FStar.Ghost.reveal FStar.Seq.Base.seq Prims.op_Subtraction FStar.Seq.Base.append FStar.Ghost.erased LowStar.Monotonic.Buffer.deref
module EverParse3d.Readable

let perm0 t = B.pointer (Ghost.erased (Seq.seq bool))

let perm_prop p b = B.loc_disjoint (B.loc_buffer b) (B.loc_buffer p) /\ True

let loc_perm p = B.loc_buffer p

let loc_perm_prop p = ()

let valid_perm h #_ #b p =
  B.live h b /\
  B.live h p /\
  Seq.length (B.deref h p) == B.length b

let valid_perm_prop h p = ()

let preserved #_ #b p from to h h' =
  (valid_perm h p /\ U32.v from <= U32.v to /\ U32.v to <= B.length b) ==>
  (valid_perm h' p /\ Seq.slice (B.deref h' p) (U32.v from) (U32.v to) `Seq.equal` Seq.slice (B.deref h p) (U32.v from) (U32.v to))

let valid_perm_frame h p l h' = ()

let preserved_refl p from to h = ()

let preserved_trans p from to h1 h2 h3 = ()
val preserved_split
  (#t: _) (#b: B.buffer t) (p: perm b)
  (from: U32.t)
  (mid: U32.t)
  (to: U32.t { U32.v from <= U32.v mid /\ U32.v mid <= U32.v to /\ U32.v to <= B.length b })
  (h h' : HS.mem)
: Lemma
  (preserved p from to h h' <==> (preserved p from mid h h' /\ preserved p mid to h h'))

    p: EverParse3d.Readable.perm b ->
    from: FStar.UInt32.t ->
    mid: FStar.UInt32.t ->
    to:
      FStar.UInt32.t
        { FStar.UInt32.v from <= FStar.UInt32.v mid /\ FStar.UInt32.v mid <= FStar.UInt32.v to /\
          FStar.UInt32.v to <= LowStar.Monotonic.Buffer.length b } ->
    h: FStar.Monotonic.HyperStack.mem ->
    h': FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
    (ensures
      EverParse3d.Readable.preserved p from to h h' <==>
      EverParse3d.Readable.preserved p from mid h h' /\ EverParse3d.Readable.preserved p mid to h h'
    )