Fix mmio Trace Test

[DavePearce]

This is reporting a failure:

   ...
   valid_corset_test.go:933: Trace rejected incorrectly (AIR, ../../testdata/mmio.accepts, line 100 with padding 7): [constraint "exo-sum-decoding" does not hold (row 20)]

This needs to be debugged and fixed.

[DavePearce]

Reduced test:

(module mmio)

(defcolumns
  (EXO_SUM :i32)
  (IS_LIMB_VANISHES :binary@prove)
  (IS_LIMB_TO_RAM_TRANSPLANT :binary@prove)
  (IS_LIMB_TO_RAM_ONE_TARGET :binary@prove)
  (IS_LIMB_TO_RAM_TWO_TARGET :binary@prove)
  (IS_RAM_TO_LIMB_TRANSPLANT :binary@prove)
  (IS_RAM_TO_LIMB_ONE_SOURCE :binary@prove)
  (IS_RAM_TO_LIMB_TWO_SOURCE :binary@prove)
  (EXO_IS_ROM :binary@prove)
  (EXO_IS_KEC :binary@prove)
  (EXO_IS_LOG :binary@prove)
  (EXO_IS_TXCD :binary@prove)
  (EXO_IS_ECDATA :binary@prove)
  (EXO_IS_RIPSHA :binary@prove)
  (EXO_IS_BLAKEMODEXP :binary@prove))

(defconst
  LLARGE                                    16
  LLARGEMO                                  (- LLARGE 1)
  ;;
  EXO_SUM_INDEX_ROM                         0
  EXO_SUM_INDEX_KEC                         1
  EXO_SUM_INDEX_LOG                         2
  EXO_SUM_INDEX_TXCD                        3
  EXO_SUM_INDEX_ECDATA                      4
  EXO_SUM_INDEX_RIPSHA                      5
  EXO_SUM_INDEX_BLAKEMODEXP                 6
  EXO_SUM_WEIGHT_ROM                        (^ 2 EXO_SUM_INDEX_ROM)
  EXO_SUM_WEIGHT_KEC                        (^ 2 EXO_SUM_INDEX_KEC)
  EXO_SUM_WEIGHT_LOG                        (^ 2 EXO_SUM_INDEX_LOG)
  EXO_SUM_WEIGHT_TXCD                       (^ 2 EXO_SUM_INDEX_TXCD)
  EXO_SUM_WEIGHT_ECDATA                     (^ 2 EXO_SUM_INDEX_ECDATA)
  EXO_SUM_WEIGHT_RIPSHA                     (^ 2 EXO_SUM_INDEX_RIPSHA)
  EXO_SUM_WEIGHT_BLAKEMODEXP                (^ 2 EXO_SUM_INDEX_BLAKEMODEXP))

(defun (weighted-exo-sum)
  (+ (* EXO_SUM_WEIGHT_ROM EXO_IS_ROM)
     (* EXO_SUM_WEIGHT_KEC EXO_IS_KEC)
     (* EXO_SUM_WEIGHT_LOG EXO_IS_LOG)
     (* EXO_SUM_WEIGHT_TXCD EXO_IS_TXCD)
     (* EXO_SUM_WEIGHT_ECDATA EXO_IS_ECDATA)
     (* EXO_SUM_WEIGHT_RIPSHA EXO_IS_RIPSHA)
     (* EXO_SUM_WEIGHT_BLAKEMODEXP EXO_IS_BLAKEMODEXP)))

(defconstraint exo-sum-decoding ()
  (eq! (weighted-exo-sum) (* (instruction-may-provide-exo-sum) EXO_SUM)))

(defun (instruction-may-provide-exo-sum)
  (force-bool (+ IS_LIMB_VANISHES
                 IS_LIMB_TO_RAM_TRANSPLANT
                 IS_LIMB_TO_RAM_ONE_TARGET
                 IS_LIMB_TO_RAM_TWO_TARGET
                 IS_RAM_TO_LIMB_TRANSPLANT
                 IS_RAM_TO_LIMB_ONE_SOURCE
                 IS_RAM_TO_LIMB_TWO_SOURCE)))

With this trace fails:

{
    "mmio.IS_LIMB_TO_RAM_TRANSPLANT": [0],
    "mmio.IS_LIMB_TO_RAM_TWO_TARGET": [0],
    "mmio.IS_LIMB_TO_RAM_ONE_TARGET": [0],    
    "mmio.IS_RAM_TO_LIMB_TRANSPLANT": [1],
    "mmio.IS_RAM_TO_LIMB_ONE_SOURCE": [0],
    "mmio.IS_RAM_TO_LIMB_TWO_SOURCE": [0],   
    "mmio.IS_LIMB_VANISHES": [0],
    "mmio.EXO_IS_BLAKEMODEXP": [0],
    "mmio.EXO_SUM": [16],
    "mmio.EXO_IS_RIPSHA": [0],
    "mmio.EXO_IS_ECDATA": [1],
    "mmio.EXO_IS_LOG": [0],
    "mmio.EXO_IS_ROM": [0],
    "mmio.EXO_IS_KEC": [0],
    "mmio.EXO_IS_TXCD": [0]
}

[DavePearce]

Minimised test:

(defcolumns
  (EXO_SUM :i32)
  (IS_RAM_TO_LIMB_TRANSPLANT :binary@prove)
  (EXO_IS_ECDATA :binary@prove))

(defconst
  EXO_SUM_INDEX_ECDATA                      4
  EXO_SUM_WEIGHT_ECDATA                     (^ 2 EXO_SUM_INDEX_ECDATA))

(defun (weighted-exo-sum) (* EXO_SUM_WEIGHT_ECDATA EXO_IS_ECDATA))
(defun (instruction-may-provide-exo-sum) (force-bool IS_RAM_TO_LIMB_TRANSPLANT))

(defconstraint exo-sum-decoding ()
  (eq! (weighted-exo-sum) (* (instruction-may-provide-exo-sum) EXO_SUM)))

With this trace:

{
    "IS_RAM_TO_LIMB_TRANSPLANT": [1],
    "EXO_SUM": [16],
    "EXO_IS_ECDATA": [1]
}

Looks like another issue with constants. Specifically, the constant EXO_SUM_WEIGHT_ECDATA looks to be incorrect somehow.