let is_subset_vec (#n: pos) (a b: bv_t n) =
  forall (i: nat). i < n ==> index b i = false ==> index a i = false
let is_subset_vec (#n: pos) (a b: bv_t n) =
forall (i: nat). i < n ==> index b i = false ==> index a i = false
FStar.BitVector.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
FStar.BitVector.fst
Prims.pos FStar.BitVector.bv_t Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.bool FStar.Seq.Base.index Prims.logical
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module FStar.BitVector

/// This module defines a bit vector as a sequence of booleans of a
/// given length, and provides various utilities.
///
/// NOTE: THE TYPE [bv_t] DEFINED IS UNRELATED TO THE SMT SOLVER'S
/// THEORY OF BIT VECTORS. SEE [FStar.BV] FOR THAT.
///
/// TODO: We might rename this module to FStar.Seq.Boolean?

open FStar.Mul
open FStar.Seq

(** [bv_t n] is just a sequence of booleans of length [n] *)
type bv_t (n: nat) = vec: seq bool {length vec = n}

(**** Common constants *)

(** A length [n] zero vector *)
let zero_vec (#n: pos) : Tot (bv_t n) = create n false

(** A vector of length [n] whose [i]th bit is set, only *)
let elem_vec (#n: pos) (i: nat{i < n}) : Tot (bv_t n) = upd (create n false) i true

(** A length [n] vector all of whose bits are set *)
let ones_vec (#n: pos) : Tot (bv_t n) = create n true

(** Bitwise logical and *)
let rec logand_vec (#n: pos) (a b: bv_t n) : Tot (bv_t n) =
  if n = 1
  then create 1 (index a 0 && index b 0)
  else append (create 1 (index a 0 && index b 0)) (logand_vec #(n - 1) (slice a 1 n) (slice b 1 n))

(** [logand] defined in terms of its indexing behavior *)
let rec logand_vec_definition (#n: pos) (a b: bv_t n) (i: nat{i < n})
    : Lemma (ensures index (logand_vec #n a b) i = (index a i && index b i))
      [SMTPat (index (logand_vec #n a b) i)] =
  if i = 0 then () else logand_vec_definition #(n - 1) (slice a 1 n) (slice b 1 n) (i - 1)

(** Bitwise logical exclusive or *)
let rec logxor_vec (#n: pos) (a b: bv_t n) : Tot (bv_t n) =
  if n = 1
  then create 1 (index a 0 <> index b 0)
  else append (create 1 (index a 0 <> index b 0)) (logxor_vec #(n - 1) (slice a 1 n) (slice b 1 n))

(** [logxor] defined in terms of its indexing behavior *)
let rec logxor_vec_definition (#n: pos) (a b: bv_t n) (i: nat{i < n})
    : Lemma (ensures index (logxor_vec #n a b) i = (index a i <> index b i))
      [SMTPat (index (logxor_vec #n a b) i)] =
  if i = 0 then () else logxor_vec_definition #(n - 1) (slice a 1 n) (slice b 1 n) (i - 1)

(** Bitwise logical or *)
let rec logor_vec (#n: pos) (a b: bv_t n) : Tot (bv_t n) =
  if n = 1
  then create 1 (index a 0 || index b 0)
  else append (create 1 (index a 0 || index b 0)) (logor_vec #(n - 1) (slice a 1 n) (slice b 1 n))

(** [logor] defined in terms of its indexing behavior *)
let rec logor_vec_definition (#n: pos) (a b: bv_t n) (i: nat{i < n})
    : Lemma (ensures index (logor_vec #n a b) i = (index a i || index b i))
      [SMTPat (index (logor_vec #n a b) i)] =
  if i = 0 then () else logor_vec_definition #(n - 1) (slice a 1 n) (slice b 1 n) (i - 1)

(** Bitwise negation *)
let rec lognot_vec (#n: pos) (a: bv_t n) : Tot (bv_t n) =
  if n = 1
  then create 1 (not (index a 0))
  else append (create 1 (not (index a 0))) (lognot_vec #(n - 1) (slice a 1 n))

(** [lognot] defined in terms of its indexing behavior *)
let rec lognot_vec_definition (#n: pos) (a: bv_t n) (i: nat{i < n})
    : Lemma (ensures index (lognot_vec #n a) i = not (index a i))
      [SMTPat (index (lognot_vec #n a) i)] =
  if i = 0 then () else lognot_vec_definition #(n - 1) (slice a 1 n) (i - 1)

(* Bitwise lemmas *)

(** If both [x] and [y] are false at a given index [i], then so is they logical xor at [i] *)
let lemma_xor_bounded (m: pos) (n: nat) (x y: bv_t m)
    : Lemma
      (requires
        (forall (i: nat).
            (i < m /\ i >= n) ==>
            (Seq.index x (m - 1 - i) = false /\ Seq.index y (m - 1 - i) = false)))
      (ensures
        (forall (i: nat). (i < m /\ i >= n) ==> (Seq.index (logxor_vec x y) (m - 1 - i) = false))) =
  ()

(** The property that the zero bits of b are also zero in a.
    I.e. that a is a subset of b. *)
val is_subset_vec : a: FStar.BitVector.bv_t n -> b: FStar.BitVector.bv_t n -> Prims.logical
a: FStar.BitVector.bv_t n -> b: FStar.BitVector.bv_t n -> Prims.logical