val quad32_xor_def (x y: quad32) : quad32
let quad32_xor_def (x y:quad32) : quad32 = four_map2 nat32_xor x y
val quad32_xor_def (x y: quad32) : quad32
let quad32_xor_def (x y: quad32) : quad32 =
four_map2 nat32_xor x y
Vale.Def.Types_s.fst.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Types_s.fst
Vale.Def.Types_s.quad32 Vale.Def.Words.Four_s.four_map2 Vale.Def.Types_s.nat32 Vale.Def.Types_s.nat32_xor
module Vale.Def.Types_s

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

unfold let nat8 = Vale.Def.Words_s.nat8
unfold let nat16 = Vale.Def.Words_s.nat16
unfold let nat32 = Vale.Def.Words_s.nat32
unfold let nat64 = Vale.Def.Words_s.nat64

let add_wrap (#n:nat) (x:natN n) (y:natN n) : natN n = if x + y < n then x + y else x + y - n
let sub_wrap (#n:nat) (x:natN n) (y:natN n) : natN n = if x - y >= 0 then x - y else x - y + n

// abstract bitwise operations on integers:
assume val iand : #n:nat -> a:natN n -> b:natN n -> natN n
assume val ixor : #n:nat -> a:natN n -> b:natN n -> natN n
assume val ior : #n:nat -> a:natN n -> b:natN n -> natN n
assume val inot : #n:nat -> a:natN n  -> natN n
assume val ishl : #n:nat -> a:natN n -> s:int -> natN n
assume val ishr : #n:nat -> a:natN n -> s:int -> natN n

// Alias
unfold let nat32_xor (x y:nat32) : nat32 = ixor x y

type twobits:eqtype = natN 4
type bits_of_byte:eqtype = four twobits

let byte_to_twobits (b:nat8) : bits_of_byte = nat_to_four_unfold 2 b

type double32:eqtype = two nat32
type quad32:eqtype = four nat32
val quad32_xor_def (x y: quad32) : quad32
x: Vale.Def.Types_s.quad32 -> y: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32