val 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)]
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)
val 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)]
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)
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.nat Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.int Prims.bool FStar.BitVector.logand_vec_definition Prims.op_Subtraction FStar.Seq.Base.slice Prims.unit Prims.l_True Prims.squash FStar.Seq.Base.index FStar.BitVector.logand_vec Prims.op_AmpAmp Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
(*
   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))
val 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)]
a: FStar.BitVector.bv_t n -> b: FStar.BitVector.bv_t n -> i: Prims.nat{i < n}
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Seq.Base.index (FStar.BitVector.logand_vec a b) i =
        (FStar.Seq.Base.index a i && FStar.Seq.Base.index b i))
      [SMTPat (FStar.Seq.Base.index (FStar.BitVector.logand_vec a b) i)]