Merge pull request #866 from hacspec/lib-proofs-bitvectors-additions

bit_vec_to_int_t

proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst

@@ -22,6 +22,10 @@ let pow2_minus_one_mod_lemma2 (n: nat) (m: nat {n <= m})
   = Math.Lemmas.pow2_le_compat m n;
     Math.Lemmas.small_div (pow2 n - 1) (pow2 m)
 
+let bit_vec_to_int_t #t (d: num_bits t) (bv: bit_vec d) = admit ()
+
+let bit_vec_to_int_t_lemma #t (d: num_bits t) (bv: bit_vec d) i = admit ()
+
 let bit_vec_to_int_t_array d bv = admit () // see issue #423
 let bit_vec_to_nat_array d bv = admit () // see issue #423
 

proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fsti

@@ -6,7 +6,7 @@ open Rust_primitives.Integers
 
 // TODO: relate `num_bits` with a notion of bounded integer
 /// Number of bits carried by an integer of type `t`
-type num_bits t = d: nat {d > 0 /\ d <= bits t /\ (signed t ==> d < bits t)}
+type num_bits t = d: nat {d > 0 /\ d <= bits t /\ (signed t ==> d <= bits t)}
 
 /// States that `x` is a positive integer that fits in `d` bits
 type bounded #t (x:int_t t) (d:num_bits t) =
@@ -58,6 +58,15 @@ let bit_vec_of_nat_array (#len: usize)
        (fun i -> get_bit_nat (Seq.index arr (i / d)) (i % d))
 #pop-options
 
+/// Transforms a bit vector to an integer
+val bit_vec_to_int_t #t (d: num_bits t) (bv: bit_vec d): int_t t
+
+/// `bit_vec_to_int_t` and `get_bit` are (modulo usize) inverse
+val bit_vec_to_int_t_lemma
+    #t (d: num_bits t) (bv: bit_vec d)
+    i
+  : Lemma (get_bit (bit_vec_to_int_t d bv) (sz i) == bv i)
+
 /// Transforms a bit vector into an array of integers
 val bit_vec_to_int_t_array #t (#len: usize) (d: num_bits t) (bv: bit_vec (v len * d))
   : Pure (t_Array (int_t t) len)