:sat all (\x -> False) xs returns True with big xs

[nano-o]

The command :sat all (\x -> False) all_states, issued on the REPL after loading the Cryptol code below, returns True.

all_ints : [_][32]
all_ints = [0x00000000..0xFFFFFFFF]

all_states : [_][2][32]
all_states = join [[[v,w] | w <- all_ints] | v <- all_ints]

[brianhuffman]

This seems to have something to do with arrays of length 2^64. This other example is probably an instance of the same bug:

Cryptol> :sat and (zero : [2^^64])
and (zero : [2 ^^ 64]) = True
(Total Elapsed Time: 0.006s, using Z3)

This formula is somehow being simplified away to nothing before it is sent to the solver:

Cryptol> :set prover=offline
Cryptol> :sat and (zero : [2^^64])
Writing to SMT-Lib file standard output...
To determine the satisfiability of the expression, use an external SMT solver.
; Automatically created by SBV on 2019-07-23 21:13:48.884542 PDT
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
; --- skolem constants ---
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(check-sat)

The concrete evaluator, on the other hand, throws a runtime error (which I think is the right thing to do in this case).

Cryptol> and (zero : [2^^64])

word too wide for memory: 18446744073709551616 bits

Lowering the array length to 2^63 elicits an error from the SBV library:

Cryptol> :sat and (zero : [2^^63])

SBV error:
Negative exponent

With prover set to offline, the SBV error furthermore causes the REPL to exit, which we should probably file as a separate bug:

Cryptol> :set prover=offline
Cryptol> :sat and (zero : [2^^63])
cryptol: Negative exponent

[brianhuffman]

I believe I've found the source of the problem: https://github.com/GaloisInc/cryptol/blob/master/src/Cryptol/Symbolic/Value.hs#L193

instance BitWord SBool SWord SInteger where
  [...]
  wordLit n x = svInteger (KBounded False (fromInteger n)) x

Here we have a use of fromInteger with a return type of Int. We should never do that. This produces the wrong result if the integer argument exceeds MAXINT.

We should also check every usage of fromInteger in the cryptol codebase, to ensure that none of them have problems with undetected wrap-around behavior.