val add (x y: t) : Pure t
  (requires (fits (v x + v y)))
  (ensures (fun z -> v z == v x + v y))
let add x y = I64.add x y
val add (x y: t) : Pure t
  (requires (fits (v x + v y)))
  (ensures (fun z -> v z == v x + v y))
let add x y =
I64.add x y
FStar.PtrdiffT.fst.checked
prims.fst.checked FStar.SizeT.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lib.fst.checked FStar.Int64.fsti.checked FStar.Int.Cast.fst.checked FStar.Int.fsti.checked FStar.Ghost.fsti.checked
FStar.PtrdiffT.fst
FStar.PtrdiffT.t FStar.Int64.add
module FStar.PtrdiffT

module Cast = FStar.Int.Cast
module I64 = FStar.Int64

open FStar.Ghost

friend FStar.SizeT

(** We assume the existence of lower and upper bounds corresponding to PTRDIFF_MIN
    and PTRDIFF_MAX, which ensure that a ptrdiff_t has at least width 16 according to
    the C standard *)
assume
val max_bound : x:erased int { x >= pow2 15 - 1 }
let min_bound : erased int = hide (- (reveal max_bound + 1))

(** We also assume that size_t is wider than ptrdiff_t *)
assume
val bounds_lemma (_:unit) : Lemma (SizeT.bound > max_bound)

let t = x:I64.t{I64.v x >= min_bound /\ I64.v x <= max_bound }

let fits x =
  FStar.Int.fits x I64.n == true /\
  x <= max_bound /\ x >= min_bound

let fits_lt x y = ()

let v x =
  I64.v x

let int_to_t (x: int) : Pure t
  (requires (fits x))
  (ensures (fun y -> v y == x))
  = I64.int_to_t x

let ptrdiff_v_inj x = ()
let ptrdiff_int_to_t_inj x = ()

let mk x = int_to_t (I16.v x)

let ptrdifft_to_sizet x =
  bounds_lemma ();
  Cast.int64_to_uint64 x
val add (x y: t) : Pure t
  (requires (fits (v x + v y)))
  (ensures (fun z -> v z == v x + v y))
x: FStar.PtrdiffT.t -> y: FStar.PtrdiffT.t -> Prims.Pure FStar.PtrdiffT.t