Question regarding BV logic in SMT files

[rod-chapman]

I have many SMT2.6 files, all of which use the "BV" logic for BitVectors, and (in particular) use the "bv2nat" function that is supported by Z3, CVC4 and CVC5.

Dolmen appears to reject this - e.g.

204 |   (ite (bvsge x (_ bv0 16)) (bv2nat x) (- (- 65536 (bv2nat x)))))
                                   ^^^^^^
Error Unbound identifier: `bv2nat`

Any workaround for this?

[Gbury]

Unfortunately, there is no current workaround, but I'm planning to work on one in the coming days.

For a bit of context: although supported by Z3, CVC4 and CVC5, bv2nat is not part of the official standard defined by the smtlib. More specifically, the theory for BV internally defines bv2nat but only so that it can be used in its semantic specification.

Until now, dolmen has strived to implement the standard, at least as a first goal, so that it could be used to check conformity against that standard. However, it appears that it's not sufficient anymore, so I'm planning to add a notion of typing extensions: these extensions would be enabled by cli flags and effectively add new functions to the typing builtins (similar to how the parsing extensions work, see #190 ).

[rod-chapman]

Understood. I'm trying to get a non-trivial program verification benchmark into the SMTComp suite. The code is cryptographic, so it has modular arithmetic and BV stuff all over the place...

[Gbury]

I should have an experimental version of dolmen that can accept bv2nat by the end of the week.

[Gbury]

Just to make sure, what would be the expected signature of the bv2nat function ?

[rod-chapman]

Not sure.... how is it declared in Z3, CVC4 and CVC5?

[bclement-ocp]

As far as I could tell when implementing these functions for Alt-Ergo, they use a family of function symbols of the form (bv2nat (_ BitVec n) Int) for all n > 0, and indexed function symbols ((_ int2bv n) Int (_ BitVec n)) for n > 0.

(I believe Z3 also supports nat2bv but CVC5 only supports int2bv because the developers didn't like nat2bv allowing negative arguments)

[hansjoergschurr]

In the cvc5 AletheLF proof signatures bv2nat and int2nat have the following signatures. This is roughly SMT-LIB 3 syntax.

(declare-const int2bv (->
  (! Int :var w)
  Int (BitVec w))
)

(declare-const bv2nat (->
  (! Int :var m :implicit)
  (BitVec m) Int)
)

[Gbury]

#208 adds a way for dolmen to accept the bv2nat and int2bv functions.

[rod-chapman]

Is this merged now?

[Gbury]

Apologies for the delay, yes it has been merged.

[Gbury]

Solved by #208

One can now use the --ext=bvconv option of the dolmen binary to allow bv2nat and int2bv.

[rod-chapman]

OK... now need to update the GitHub action associated with the smtcomp benchmark_submission repo so it will run the new binary with that option. Any idea how to do that?

[Gbury]

I had a look at the smt-comp repo, and its github actions will need a bit more code than currently to use the dev version of dolmen (since there is no release including PR#208 yet). You basically need two changes:

• First, the github action downloads the release binary for version 0.9, see these lines. Instead, you'll need to build the latest dev version of dolmen (or wait until I make a new release including the bvconv extension). To do that, build steps along these lines should be work (though I have not tested these):

# Setup ocaml/opam
    - name: Setup ocaml/opam
      uses: avsm/setup-ocaml@v2
      with:
        ocaml-compiler: ocaml-base-compiler.4.14.0
# Run opam udpate to get an up-to-date repo
    - name: Update opam repo
      run: opam update
# Install dev version of dolmen
   - name: Install dolmen
     run: opam pin --dev-repo dolmen dolmen_type dolmen_loop dolmen_model dolmen_bin
# Copy the dolmen binary
   - name: Copy the dolmen binary
     run: cp `opam exec -- which dolmen` ./dolmen-linux-amd64

Alternatively, I could try and see how to setup a github actions file that would build and upload a nightly release of dolmen (that wya, only the download url for the dolmen binary would need to change), but last time I looked, it was quite a bit of work.

• Second, you'll need to add the adequate extension on this line. Just adding --ext=bvconv should be enough.

[rod-chapman]

I think it's best for us to wait for the next formal binary release. Many thanks for all your efforts.