val will_add_overflow64 (x y: U64.t)
    : res: bool{res <==> not (FStar.UInt.fits (U64.v x + U64.v y) 64)}
val will_add_overflow64 (x y: U64.t)
    : res: bool{res <==> not (FStar.UInt.fits (U64.v x + U64.v y) 64)}
let will_add_overflow64 (x y:U64.t)
  : res:bool{
       res <==> not (FStar.UInt.fits (U64.v x + U64.v y) 64)
    }
  = let open U64 in
    (0xffffffffffffffffuL -^ x) <^ y
module Zeta.Steel.Util
open Steel.ST.Util
module A = Steel.ST.Array
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast

let full = Steel.FractionalPermission.full_perm
let half = Steel.FractionalPermission.half_perm full
let larray t (n:U32.t) = A.larray t (U32.v n)
[@@__steel_reduce__;__reduce__]
let array_pts_to #t (a:A.array t) (v:Seq.seq t) = A.pts_to a full_perm v

let sum_halves : squash (sum_perm half half == full) = ()

inline_for_extraction
let will_add_overflow32 (x y:U32.t)
  : res:bool{
       res <==> not (FStar.UInt.fits (U32.v x + U32.v y) 32)
    }
  = let open U32 in
    (0xfffffffful -^ x) <^ y

let check_overflow_add32 (x y:U32.t)
  : Pure (option U32.t)
    (requires True)
    (ensures fun res ->
        if FStar.UInt.fits (U32.v x + U32.v y) 32
        then Some? res /\
             Some?.v res == U32.add x y
        else None? res)
 = if will_add_overflow32 x y
   then None
   else Some U32.(x +^ y)
/
Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked
Zeta.Steel.Util.fst
x: FStar.UInt64.t -> y: FStar.UInt64.t
  -> res:
    Prims.bool
      {res <==> Prims.op_Negation (FStar.UInt.fits (FStar.UInt64.v x + FStar.UInt64.v y) 64)}
FStar.UInt64.t FStar.UInt64.op_Less_Hat FStar.UInt64.op_Subtraction_Hat FStar.UInt64.__uint_to_t Prims.bool Prims.l_iff Prims.b2t Prims.op_Negation FStar.UInt.fits Prims.op_Addition FStar.UInt64.v
let will_add_overflow64 (x y: U64.t)
    : res: bool{res <==> not (FStar.UInt.fits (U64.v x + U64.v y) 64)} =
  
let open U64 in (0xffffffffffffffffuL -^ x) <^ y