Fix failing wcp trace

[DavePearce]

There appears to be a failing trace for the wcp example which doesn't fail for the original corset tool. Some notes:

• Corresponds to the test ReplayTests_simpleSelfDestruct
• Example failing trace from testdata/wcp.accepts is line 1806
• The failing constraints is bits-and-negs

[DavePearce]

Here's the minimal test for reproduction:

(module wcp)

(defcolumns
  (COUNTER :byte)
  (IS_SLT :binary@prove)
  (IS_SGT :binary@prove)
  (BITS :binary@prove)
  (NEG_1 :binary@prove)
  (NEG_2 :binary@prove)
  (BYTE_1 :byte@prove)
  (BYTE_3 :byte@prove))

;; aliases
(defalias CT       COUNTER)

;; opcode values
(defconst
  LLARGE                                    16
  LLARGEMO                                  (- LLARGE 1))

(defun (first-eight-bits-bit-dec)
  (reduce +
          (for i
               [0 :7]
               (* (^ 2 i)
                  (shift BITS
                         (- 0 (+ i 8)))))))

(defun (last-eight-bits-bit-dec)
  (reduce +
          (for i
               [0 :7]
               (* (^ 2 i)
                  (shift BITS (- 0 i))))))

(defconstraint bits-and-negs (:guard (+ IS_SLT IS_SGT))
  (if-eq CT LLARGEMO
         (begin (eq! (shift BYTE_1 (- 0 LLARGEMO))
                     (first-eight-bits-bit-dec))
                (eq! (shift BYTE_3 (- 0 LLARGEMO))
                     (last-eight-bits-bit-dec))
                (eq! NEG_1
                     (shift BITS (- 0 LLARGEMO)))
                (eq! NEG_2
                     (shift BITS (- 0 7))))))

And a minimal failing trace is attached (wcp.minimal.json).

[DavePearce]

Seems to be something to do with this:

(defconst
  LLARGE                                    16
  LLARGEMO                                  (- LLARGE 1))

Here, changing LLARGEMO to 15 ... and it passes.