bitvector encoding brittle

[mtzguido]

open FStar.BV

// let _ : bv_t 128 = bv_zero

let int2bv_uext_64_128 (x1 : nat) :
  Lemma  (requires x1 < pow2 64) // (FStar.UInt.size x1 64))
         (ensures bv_uext #64 #64 (int2bv #64 x1) == int2bv #128 x1) =
  admit ()

Gives:

* Error 276 at Basic.fst(10,0-14,10):
  - Unexpected output from Z3:
      "(error "line 11230 column 90: unknown function/constant BoxBitVec128")"

* Error 276 at Basic.fst(10,0-14,10):
  - Unexpected output from Z3:
      "(error "line 11284 column 90: unknown function/constant BoxBitVec128")"

* Error 276 at Basic.fst(10,0-14,10):
  - Unexpected output from Z3:
      "(error "line 11338 column 90: unknown function/constant BoxBitVec128")"

* Error 276 at Basic.fst(10,0-14,10):
  - Unexpected output from Z3:
      "(error "line 11394 column 90: unknown function/constant BoxBitVec128")"

* Error 276 at Basic.fst(10,0-14,10):
  - Unexpected output from Z3:
      "(error "line 11547 column 79: unknown function/constant BoxBitVec128")"

Verified module: Basic
5 errors were reported (see above)

Uncommenting the definition of that vector makes the encoding kick in.

[amosr-msft]

Hi,
I've just run into this issue as well, when mixing definitions that are parametric in the bitwidth with concrete bitwidths. The same _: bv_t 5 trick works to remove the errors, but I've noticed that in my version, it still can't prove the property. I can prove the property if I use a tactic to unfold the parametric definitions.

module Test.BV.Abstract
(*
  Testing bitvectors with known concrete widths, compared to unknown widths.
  There seem to be difficulties converting between (bv_t 5) and (n = 5 ... |- bv_t n)
*)

module BV = FStar.BV
module U  = FStar.UInt

(* Set specific bit specialised to width=4 *)
let bit2bv_4 (bit: nat { bit < 4 }) (b: bool): BV.bv_t 4 =
  if b then BV.bvshl (BV.int2bv #4 1) bit else BV.int2bv #4 0

(* Extend a bitvector by one *)
let bv_ext1 (wy: pos) (y: BV.bv_t wy): BV.bv_t (1 + wy) =
  BV.bv_uext #wy #1 y

(* This function only uses the specialised 4-bit version, so all the definitions should use SMT-lib bitvec 4 *)
let use_concrete (n: bool): BV.bv_t 4 =
  bit2bv_4 0 n

(* This function uses the generic function, so it's unlikely to use SMT-lib bit vectors *)
let use_abstract (n: bool): BV.bv_t 5 =
  bv_ext1 4 (BV.int2bv (if n then 1 else 0))

(* When we state a lemma that uses both use_concrete and use_abstract, we run into encoding issues.
   The lemma below gives errors like:
    > - Unexpected output from Z3:
    >    "(error "line 75550 column 97: unknown function/constant BoxBitVec5")"
*)

(* Uncommenting the following definition stops the error, but it still isn't proved *)
// let _: BV.bv_t 5 = BV.bv_zero

let lemma_use_both (n: bool):
  Lemma (use_abstract n == BV.bv_uext #4 #1 (use_concrete n)) =
  (* Unfolding the definition of use_abstract and bv_msb_ext forces the native bit-vector encoding, so it can be proved *)
  // assert (use_abstract n == BV.bv_uext #4 #1 (use_concrete n))
  //   by (FStar.Tactics.norm [delta; zeta_full; iota; primops; nbe];
  //       FStar.Tactics.dump "X"
  //   )
  // ;
    ()