let lo64_reveal = opaque_revealer (`%lo64) lo64 lo64_def
let lo64_reveal =
opaque_revealer (`%lo64) lo64 lo64_def
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.Opaque_s.opaque_revealer Vale.Def.Types_s.quad32 Vale.Def.Words_s.nat64 Vale.Arch.Types.lo64 Vale.Arch.Types.lo64_def
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))

let quad32_shl32 (q:quad32) : quad32 =
  let Mkfour v0 v1 v2 v3 = q in
  Mkfour 0 v0 v1 v2

let add_wrap_quad32 (q0 q1:quad32) : quad32 =
  let open Vale.Def.Words_s in
  Mkfour (add_wrap q0.lo0 q1.lo0)
         (add_wrap q0.lo1 q1.lo1)
         (add_wrap q0.hi2 q1.hi2)
         (add_wrap q0.hi3 q1.hi3)

val lemma_BitwiseXorCommutative (x y:nat32) : Lemma (x *^ y == y *^ x)
val lemma_BitwiseXorWithZero (n:nat32) : Lemma (n *^ 0 == n)
val lemma_BitwiseXorCancel (n:nat32) : Lemma (n *^ n == 0)
val lemma_BitwiseXorCancel64 (n:nat64) : Lemma (ixor n n == 0)
val lemma_BitwiseXorAssociative (x y z:nat32) : Lemma (x *^ (y *^ z) == (x *^ y) *^ z)

val xor_lemmas (_:unit) : Lemma
  (ensures
    (forall (x y:nat32).{:pattern (x *^ y)} x *^ y == y *^ x) /\
    (forall (n:nat32).{:pattern (n *^ 0)} n *^ 0 == n) /\
    (forall (n:nat32).{:pattern (n *^ n)} n *^ n == 0) /\
    (forall (n:nat64).{:pattern (ixor n n)} ixor n n == 0) /\
    (forall (x y z:nat32).{:pattern (x *^ (y *^ z))} x *^ (y *^ z) == (x *^ y) *^ z)
  )

val lemma_quad32_xor (_:unit) : Lemma (forall q . {:pattern quad32_xor q q} quad32_xor q q == Mkfour 0 0 0 0)

let quad32_double_lo (q:quad32) : double32 = (four_to_two_two q).lo
let quad32_double_hi (q:quad32) : double32 = (four_to_two_two q).hi

val lemma_reverse_reverse_bytes_nat32 (n:nat32) :
  Lemma (reverse_bytes_nat32 (reverse_bytes_nat32 n) == n)
  [SMTPat (reverse_bytes_nat32 (reverse_bytes_nat32 n))]

val lemma_reverse_bytes_quad32 (q:quad32) :
  Lemma (reverse_bytes_quad32 (reverse_bytes_quad32 q) == q)
  [SMTPat (reverse_bytes_quad32 (reverse_bytes_quad32 q))]

val lemma_reverse_bytes_quad32_zero (_:unit) : Lemma
  (let z = Mkfour 0 0 0 0 in
   reverse_bytes_quad32 z == z)

val lemma_reverse_reverse_bytes_nat32_seq (s:seq nat32) :
  Lemma (reverse_bytes_nat32_seq (reverse_bytes_nat32_seq s) == s)
  [SMTPat (reverse_bytes_nat32_seq (reverse_bytes_nat32_seq s))]

unfold let quad32_to_seq (q:quad32) : seq nat32 = four_to_seq_LE q

val lemma_insert_nat64_properties (q:quad32) (n:nat64) :
  Lemma ( (let q' = insert_nat64 q n 0 in
            q'.hi2 == q.hi2 /\
            q'.hi3 == q.hi3) /\
           (let q' = insert_nat64 q n 1 in
            q'.lo0 == q.lo0 /\
            q'.lo1 == q.lo1))
  [SMTPat (insert_nat64 q n)]

val lemma_insert_nat64_nat32s (q:quad32) (n0 n1:nat32) :
  Lemma ( insert_nat64 q (two_to_nat32 (Mktwo n0 n1)) 0 ==
          Mkfour n0 n1 q.hi2 q.hi3 /\
          insert_nat64 q (two_to_nat32 (Mktwo n0 n1)) 1 ==
          Mkfour q.lo0 q.lo1 n0 n1 )

let lo64_def (q:quad32) : nat64 = two_to_nat 32 (two_select (four_to_two_two q) 0)
val lo64_reveal : _: Prims.unit -> FStar.Pervasives.Lemma (ensures Vale.Arch.Types.lo64 == Vale.Arch.Types.lo64_def)
_: Prims.unit -> FStar.Pervasives.Lemma (ensures Vale.Arch.Types.lo64 == Vale.Arch.Types.lo64_def)