Kernel crash - relating to finiteSeqMap

[linesthatinterlace]

I have the following functions:

zero_from : {m, a, b} (Logic a, Eq a, fin m, Integral b,  Literal 1 b, Cmp b) => b -> [m]a -> Bit
zero_from N xs = zipWith (&&) (take <~ finite_support N) xs == zero
  where finite_support n = if n <= 0 then repeat (~zero) else [zero] # finite_support (n - 1)

zero_from' : {m, a, b} (Zero a, Eq a, fin m, Integral b, Cmp b, LiteralLessThan m b) => b -> [m]a -> Bit
zero_from' N xs = and [ xs@(index i) == zero | i <- [0 .. <m] ]
  where index i = max N i

zero_from_eq : {n, a, b} (Cmp a, Eq b, Integral a, Logic b, LiteralLessThan n a, Literal (max 1 n) a, Literal 1 a, fin n) => a -> [n]b -> Bit
property zero_from_eq N xs = (N < `n) ==> zero_from N xs == zero_from' N xs

When running the following command with :prover = w4-yices, I get the following error message, which asks me to create an issue here. :prove \(N : Integer) -> zero_from_eq N ([0] : [1][0])

What4 exception:
You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  74fe8bebc4b547664eea6b3df9936f0bc8ba4e1b
  Branch:    release-2.11.0 (uncommited files present)
  Location:  finiteSeqMap
  Message:   Out of bounds access of finite seq map
             length: 1
             1
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.11.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Value.hs:154:14 in cryptol-2.11.0-inplace:Cryptol.Eval.Value
%< --------------------------------------------------- 

Note that running it with :prover = yices gives the following:

SBV exception:

*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (define-fun s13 () (_ BitVec 0) #x0)
***    Expected  : success
***    Received  : (error "at line 7, column 30: size must be positive in BitVec")
***
***    Exit code : ExitSuccess
***    Executable: /usr/bin/yices-smt2
***    Options   : --incremental
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

Running it with :prover = offline gives:

Writing to SMT-Lib file standard output...
To determine the validity of the expression, use an external SMT solver.
; Automatically created by SBV on 2021-06-14 12:08:50.3929814 BST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic ALL) ; has unbounded values, using catch-all.
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
(define-fun s1 () Int 1)
(define-fun s3 () Int 0)
(define-fun s12 () (_ BitVec 1) #b1)
(define-fun s13 () (_ BitVec 0) #x0)
; --- skolem constants ---
(declare-fun s0 () Int)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s2 () Bool (< s0 s1))
(define-fun s4 () Bool (> s0 s3))
(define-fun s5 () Int (ite s4 s0 s3))
(define-fun s6 () Bool (< s5 s3))
(define-fun s7 () Bool (not s6))
(define-fun s8 () Bool (< s5 s1))
(define-fun s9 () Bool (and s7 s8))
(define-fun s10 () Bool (not s2))
(define-fun s11 () Bool (or s9 s10))
(assert (not s11))
(check-sat)

And running it with :prove = w4-offline gives:

cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  74fe8bebc4b547664eea6b3df9936f0bc8ba4e1b
  Branch:    release-2.11.0 (uncommited files present)
  Location:  finiteSeqMap
  Message:   Out of bounds access of finite seq map
             length: 1
             1
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.11.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Value.hs:154:14 in cryptol-2.11.0-inplace:Cryptol.Eval.Value
%< --------------------------------------------------- 

This last one, incidentally, crashes Cryptol entirely and dumps me to the command line.

:set prover = mathsat works and proves it. :set prover = z3 just seems to hang, but maybe it would have succeeded had I waited.

So there's two things going on here, maybe, which are probably related:

• SBV produces SMT-Lib2 which provokes a failure response from Yices but which MathSAT can handle - so maybe it's malformed but good.
• What4 cannot cope with this and crashes. So maybe this is a What4 bug? Nevertheless, the output asked me to raise it here so I'm doing so in the name of being a helpful user.

Obviously I think what these functions are doing is quite weird, so something is being stress-tested I guess! Thought you'd rather know.

[robdockins]

What is the definition of (<~)

[robdockins]

I think i figured out that

(<~) : {a, b} (a -> b) -> a -> b
f <~ x = f x

In current master, the What4 backends are working properly and prove the property (which I think is the expected behavior).

The SBV backends, however, are still asking solvers to reason about 0-bit bitvectors, which are not allowed by the SMTLib standard. MathSAT appears to be accepting the query anyway, but the other solvers are (correctly) rejecting these queries.

[linesthatinterlace]

Oh, sorry, I didn't notice I'd used that. Yes - I define <~ and ~~> to do the equivalent of Haskell's $ and . because they are so consistently useful, I forget they aren't core Lean.

Aha - I am using I think the latest numbered release of Cryptol, but the current version has since fixed this (and so it'll be fixed next release)?

[robdockins]

It seems fixed for What4, although I'm interested in tracking down exactly what fixed it. For SBV, it's still a problem; I'll have to see if we can engineer a relatively easy fix.

[linesthatinterlace]

I'm not certain now that's it's solely about zero-bit bitvectors though I'm unable to check at this time - I can't remember what values it was crashing with and should have included more, I suppose. It might just have been that though.

[brianhuffman]

Here's a smaller example that seems to trigger the same bug:

:prove \(i:[1]) -> (zero:[2][0])@i == zero

With :set prover=yices, I get this error message:

SBV exception:

*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (define-fun s1 () (_ BitVec 0) #x0)
***    Expected  : success
***    Received  : (error "at line 4, column 29: size must be positive in BitVec")
***
***    Exit code : ExitSuccess
***    Executable: /Users/huffman/.bin/yices-smt2
***    Options   : --incremental
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

[robdockins]

Well, we have already implemented the easy tricks that I thought might help with this issue.

A proper solution to this will require altering the SBV backend representation of bitvectors to add a new dummy 0-bit-wide value, similar to what we are already doing for What4. However, I'm somewhat inclined to just implement #1132 instead, which would unify the What4 and SBV code for handling these issues, and others.