val 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)
val 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)
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)
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
/
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.UInt32.t -> y: FStar.UInt32.t -> Prims.Pure (FStar.Pervasives.Native.option FStar.UInt32.t)
FStar.UInt32.t Zeta.Steel.Util.will_add_overflow32 FStar.Pervasives.Native.None Prims.bool FStar.Pervasives.Native.Some FStar.UInt32.op_Plus_Hat FStar.Pervasives.Native.option Prims.l_True FStar.UInt.fits Prims.op_Addition FStar.UInt32.v Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.eq2 FStar.Pervasives.Native.__proj__Some__item__v FStar.UInt32.add FStar.Pervasives.Native.uu___is_None
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)