val quad32_shl32 (q: quad32) : quad32
let quad32_shl32 (q:quad32) : quad32 =
  let Mkfour v0 v1 v2 v3 = q in
  Mkfour 0 v0 v1 v2
val quad32_shl32 (q: quad32) : quad32
let quad32_shl32 (q: quad32) : quad32 =
let Mkfour v0 v1 v2 v3 = q in
Mkfour 0 v0 v1 v2
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.Types_s.quad32 Vale.Def.Types_s.nat32 Vale.Def.Words_s.Mkfour
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
unfold let add_wrap64 (x:nat64) (y:nat64) : nat64 = add_wrap x y
unfold let sub_wrap32 (x:nat32) (y:nat32) : nat32 = sub_wrap x y
unfold let sub_wrap64 (x:nat64) (y:nat64) : nat64 = sub_wrap x y

unfold let iand32 (a:nat32) (b:nat32) : nat32 = iand a b
unfold let ixor32 (a:nat32) (b:nat32) : nat32 = ixor a b
unfold let ior32 (a:nat32) (b:nat32) : nat32 = ior a b
unfold let inot32 (a:nat32) : nat32 = inot a
unfold let ishl32 (a:nat32) (s:int) : nat32 = ishl a s
unfold let ishr32 (a:nat32) (s:int) : nat32 = ishr a s

unfold let iand64 (a:nat64) (b:nat64) : nat64 = iand a b
unfold let ixor64 (a:nat64) (b:nat64) : nat64 = ixor a b
unfold let ior64 (a:nat64) (b:nat64) : nat64 = ior a b
unfold let inot64 (a:nat64) : nat64 = inot a
unfold let ishl64 (a:nat64) (s:int) : nat64 = ishl a s
unfold let ishr64 (a:nat64) (s:int) : nat64 = ishr a s

unfold let iand128 (a:nat128) (b:nat128) : nat128 = iand a b
unfold let ixor128 (a:nat128) (b:nat128) : nat128 = ixor a b
unfold let ior128 (a:nat128) (b:nat128) : nat128 = ior a b
unfold let inot128 (a:nat128) : nat128 = inot a
unfold let ishl128 (a:nat128) (s:int) : nat128 = ishl a s
unfold let ishr128 (a:nat128) (s:int) : nat128 = ishr a s

unfold let two_to_nat32 (x:two nat32) : nat64 = two_to_nat 32 x

val lemma_nat_to_two32 (_:unit) : Lemma
  (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))
val quad32_shl32 (q: quad32) : quad32
q: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32