val nth_zero_eq_lemma2: #n:pos -> a:UInt.uint_t n ->
  Lemma
  ((forall (i:nat{i<n}). UInt.nth a i = false) ==> (a == UInt.zero n))
val nth_zero_eq_lemma2: #n:pos -> a:UInt.uint_t n ->
  Lemma
  ((forall (i:nat{i<n}). UInt.nth a i = false) ==> (a == UInt.zero n))
let nth_zero_eq_lemma2 #n a =
  // This proof is insanely complex because of problems with pattern matching...
  let foralli_eq a = (forall (i:nat{i<n}). UInt.nth #n a i = false) in
  let eq (a b : UInt.uint_t n) = (a = b) in
  let l a :
  Lemma
  (requires (foralli_eq a))
  (ensures (eq a (UInt.zero n)))
  [SMTPat (eq a (UInt.zero n))] =
  nth_zero_eq_lemma2_aux #n a
  in
  assert(foralli_eq a <==> eq a (UInt.zero n))
module Impl.Noise.BufferEquality

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

open Lib.Sequence
module S = Lib.Sequence
module L = FStar.List
module Seq = FStar.Seq

open Lib.Buffer
open LowStar.BufferOps

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module G = FStar.Ghost

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"

(*** Buffer equality *)
// TODO: move?
val logxor_uint_eq_zero_lem :#t:inttype{unsigned t} -> #l:secrecy_level -> a:uint_t t l -> b:uint_t t l ->
  Lemma (logxor a b == zeros t l <==> a == b)

let logxor_uint_eq_zero_lem #t #l a b =
  assert(v (zeros t l) = 0);
  UInt.logxor_neq_nonzero #(bits t) (v a) (v b);
  assert(
    Lib.IntTypes.v a <> Lib.IntTypes.v b ==>
    UInt.logxor #(bits t) (Lib.IntTypes.v a) (Lib.IntTypes.v b) <> 0);
  logxor_spec a b;
  assert(v a <> v b ==> v (logxor a b) <> 0);
  assert((~(a == b)) ==> v (logxor a b) <> 0);
  UInt.logxor_self #(bits t) (v a);
  logxor_spec a a

val logxor_commutative: #t:inttype{unsigned t} -> #l:secrecy_level -> a:uint_t t l -> b:uint_t t l ->
  Lemma (requires True) (ensures (logxor a b == logxor b a))

let logxor_commutative #t #l a b =
  logxor_spec a b;
  logxor_spec b a;
  UInt.logxor_commutative #(bits t) (v a) (v b)

val logxor_associative: #t:inttype{unsigned t} -> #l:secrecy_level -> a:uint_t t l -> b:uint_t t l -> c:uint_t t l ->
  Lemma (requires True) (ensures (logxor (logxor a b) c == logxor a (logxor b c)))

let logxor_associative #t #l a b c =
  logxor_spec a b;
  logxor_spec b c;
  logxor_spec (logxor a b) c;
  logxor_spec a (logxor b c);
  UInt.logxor_associative #(bits t) (v a) (v b) (v c)

val logor_eq_zero_i (#n:pos) (a:UInt.uint_t n) (b:UInt.uint_t n) (i : nat{i < n}) :
  Lemma (requires True)
  (ensures (
    UInt.nth (UInt.logor a b) i == false <==>
    (UInt.nth a i == false /\
     UInt.nth b i == false)))
  [SMTPat (UInt.nth (UInt.logor a b) i)]

let logor_eq_zero_i #n a b i = ()

module BV = FStar.BitVector

val nth_zero_eq_lemma1: #n:pos -> a:UInt.uint_t n ->
  Lemma (a == UInt.zero n ==> (forall (i:nat{i<n}). UInt.nth a i = false))

let nth_zero_eq_lemma1 #n a = ()

val nth_zero_eq_lemma2_aux: #n:pos -> a:UInt.uint_t n ->
  Lemma
  (requires (forall (i:nat{i<n}). UInt.nth a i = false))
  (ensures (a == UInt.zero n))

let nth_zero_eq_lemma2_aux #n a =
  let lemi (i:nat{i<n}) :
    Lemma(UInt.nth a i = UInt.nth (UInt.zero n) i)
    [SMTPat (UInt.nth a i)] =
    assert(UInt.nth a i = false);
    UInt.zero_nth_lemma #n i
  in
  assert(forall (i:nat{i<n}). UInt.nth a i = UInt.nth (UInt.zero n) i);
  UInt.nth_lemma #n a (UInt.zero n)

val nth_zero_eq_lemma2: #n:pos -> a:UInt.uint_t n ->
  Lemma
  ((forall (i:nat{i<n}). UInt.nth a i = false) ==> (a == UInt.zero n))
/
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Loops.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt128.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.Int.Cast.Full.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.BitVector.fst.checked
Impl.Noise.BufferEquality.fst
a: FStar.UInt.uint_t n
  -> FStar.Pervasives.Lemma
    (ensures (forall (i: Prims.nat{i < n}). FStar.UInt.nth a i = false) ==> a == FStar.UInt.zero n)
Prims.pos FStar.UInt.uint_t Prims._assert Prims.l_iff Prims.b2t FStar.UInt.zero Prims.unit Prims.squash Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.bool Prims.Nil Impl.Noise.BufferEquality.nth_zero_eq_lemma2_aux Prims.op_Equality Prims.logical Prims.l_Forall Prims.nat Prims.op_LessThan FStar.UInt.nth
let nth_zero_eq_lemma2 #n a =
  
let foralli_eq a = (forall (i: nat{i < n}). UInt.nth #n a i = false) in
let eq (a b: UInt.uint_t n) = (a = b) in
let l a
    : Lemma (requires (foralli_eq a)) (ensures (eq a (UInt.zero n))) [SMTPat (eq a (UInt.zero n))] =
  nth_zero_eq_lemma2_aux #n a
in
assert (foralli_eq a <==> eq a (UInt.zero n))