val sub_wrap32 (x y: nat32) : nat32
let sub_wrap32 (x:nat32) (y:nat32) : nat32 = sub_wrap x y
val sub_wrap32 (x y: nat32) : nat32
let sub_wrap32 (x y: nat32) : nat32 =
sub_wrap x y
Vale.Arch.Types.fsti.checked
Vale.Lib.Seqs_s.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Arch.Types.fsti
Vale.Def.Words_s.nat32 Vale.Def.Types_s.sub_wrap Vale.Def.Words_s.pow2_32
module Vale.Arch.Types

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Lib.Seqs_s
open Vale.Lib.Seqs
open Vale.Def.Words_s
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Seq
open FStar.Seq
open Vale.Def.Words.Two_s

unfold let ( *^ ) = nat32_xor
unfold let ( *^^ ) = quad32_xor

unfold let add_wrap32 (x:nat32) (y:nat32) : nat32 = add_wrap x y
val sub_wrap32 (x y: nat32) : nat32
x: Vale.Def.Words_s.nat32 -> y: Vale.Def.Words_s.nat32 -> Vale.Def.Words_s.nat32