muxBVal: VInt (0, 1)

[weaversa]

I'm hitting this fail in BitBlast.hs when running write_aig. In my run, x and y are 0 and 1.

muxInt _ x y = if x == y then return x else fail $ "muxBVal: VInt " ++ show (x, y)

I can try to get an example if necessary. Oddly enough, a .aig file is produced, but I'm afraid to trust that it's correct.

[weaversa]

Here is an example:

$ more test.cry
hasRepeat : {a, b} (fin a, a >= 2, Eq b) => [a]b -> b -> Integer -> Bit
hasRepeat xs b num = out == num
  where
    out = foldl (\a x -> if a == num then num
                          | x == b   then a+1
                         else 0) 0 xs
$ saw
sawscript> write_aig "test.aig" {{ \(x : [10]) -> hasRepeat x True 2 }}

Stack trace:
"write_aig" (<stdin>:1:1-1:10):
muxBVal: VInt (1,0)

[atomb]

I wouldn't expect that we'd be able to write an AIG file from a Cryptol function that involves the Integer type. If I change the Integer to some bitvector type ([8] in my example), it seems to work. Is that a workable solution in the situation where you're encountering this?

[atomb]

Perhaps needless to say, though: we should be giving a better error message in the case of trying to bitblast something that can't be represented in a fixed number of bits.

[brianhuffman]

Some cryptol functions that involve the Integer type are able to be bit-blasted: The important thing is that all intermediate Integer values must be possible to evaluate concretely and not depend on any input values. For example, a function that is defined using generate with an Integer index type should be fine. In this particular example, the intermediate value out has type Integer, and also clearly depends on the symbolic input xs, so it definitely can't be bit-blasted.

I wonder how hard it would be to implement a syntactic check for this property?

[weaversa]

Thanks! I figured something like that was going on, but felt it should work because term_theories claimed the term only relied on "Bitvectors". Could term_theories be strengthened a bit to include when Integer is also needed?

sawscript> term_theories [] {{ \(a : [10]) -> hasRepeat a True 4 }}
[16:40:41.138] ["Bitvectors"]
sawscript> write_aig "test.aig" {{ \(a : [10]) -> hasRepeat a True 4 }}

Stack trace:
"write_aig" (<stdin>:1:1-1:10):
muxBVal: VInt (1,0)

[brianhuffman]

The REPL documentation for term_theories says:

Note: the given term will be simplified using the What4 backend
before evaluating what theories are required.  For simple problems,
this may simplify away some aspects of the problem altogether and may result
in requiring fewer theories than one might expect.

I expect that this is exactly what is happening here. What4 is probably simplifying some of the combinations of integer-equality and if-then-else to the point that all uses of Integer are simplified away. The problem is that write_aig doesn't do any such simplification. We should reimplement write_aig to go via What4 so that it will actually work with any term that term_theories says is boolean-only.

Actually, we should probably go a step further: write_aig should actually be implemented by essentially running term_theories on the given term, but also saving the resulting simplified what4 expression. If it requires any non-boolean theories, then we can print a nice error message saying so. If the simplified what4 term only needs boolean reasoning, then we can generate an aig file from the simplified what4 term.

I'm not sure whether we have an AIG backend for What4 yet. If we do, then we should switch write_aig to use it. If not, then we should make one.

[brianhuffman]

Yes, we do have an AIG backend for What4; it's in the what4-abc package. We could probably switch all our SAW bit-blasting to go through what4-abc instead of going directly from SAW. That would make all of the abc-related proof commands work on any term or proof goal that term_theories says is boolean-only. We likely wouldn't need the saw-core-aig package any more.

[atomb]

The what4-abc package currently links in the ABC library to do the work, which is just what we've just managed to remove from SAW. However, I think we could rework it to use the pure Haskell AIG writing code from the aig package (which uses the same interface it's already using) and then I think we could indeed drop the saw-core-aig package. Going through What4 before AIG just seems like it makes more sense anyway.

[atomb]

It's not at all clear to me, offhand, why saw-core-what4 is able to simplify away the uses of Integer in that example and saw-core-aig isn't.

[brianhuffman]

Evaluating the foldl in the posted example produces a bunch of instances of the pattern (if b then x else y) == z at type Integer. In the saw-core-aig backend, evaluating the if b then x else y subterm already fails, because b is a symbolic boolean and x and y are not equal constants. The problem is that saw-core-aig is using the plain haskell type Integer to represent symbolic expressions of saw-core type Integer, so basically it fails unless every Integer subexpression evaluates concretely.

saw-script/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

Line 98 in 354cda0

type instance VInt (BitBlast l) = Integer

In saw-core-what4, on the other hand, the left-hand side successfully evaluates to a mux tree, and then I believe the equality comparison gets pushed into the leaves, producing something like if b then x == z else y == z. With the equalities pushed all the way in, they can get simplified away, leaving nothing but booleans.

[brianhuffman]

I suppose we could enhance saw-core-aig by reimplementing VInt (BitBlast l) to use some kind of mux-tree datatype instead of just Integer. But we've already done the work to implement that in What4, so it's probably better to just use What4 instead of duplicating that work.

[robdockins]

I agree, I think it makes more sense to just use What4 here rather than reimplement mux-trees in saw-core-aig. We have a couple of ways we can go here. I think the easiest is to change what4-abc to use the compact graph representation from the aig package instead of relying on abcBridge; then, slot that in in place of saw-core-aig.

[robdockins]

Given the issues described in #1492, I'm no longer sure it makes sense to just reimplement saw-core-aig. As a workaround, perhaps we can implement a term_eval primitive that does a round-trip via What4 (the same way that goal_eval does, and using the same mechanism as term_theories) so that we can get the benefits of What4 simplification when we want them.

[RyanGlScott]

There are several tasks here:

1. The example in muxBVal: VInt (0, 1) #1436 (comment) panics. We should improve the error handling to avoid this.
2. As proposed in muxBVal: VInt (0, 1) #1436 (comment), we should introduce a term_eval : Term -> Term primitive that performs round-trip evaluation via What4. This is being done in Add saw-script functions term_eval and term_eval_unint. #927.
3. After completing (2), we should see if write_aig "test.aig" (term_eval {{ \(a : [10]) -> hasRepeat a True 4 }}) succeeds.