Constant columns in lookups

[OlivierBBB]

Main issue

In lookups it is sometimes useful to have constant columns, typically a zero column (say when in an instruction sent to WCP or to MOD the HIGH part of one of the two arguments or results is known to always be zero.)

Current solution

Currently the solution we use is to add a constant column to the module and constrain it to be zero. This allows us to call it within a lookup. E.g.

(defcolumns
  ...
  ZERO
)

with a constraint à la

(defconstraint zero-col () (vanishes! ZERO))

So that in the lookup we may call it e.g. like this

(defplookup stp-into-mod
    ; target columns (in MOD)
    (
        mod.ARG_1_HI
        mod.ARG_1_LO
        mod.ARG_2_HI
        mod.ARG_2_LO
        mod.RES_HI
        mod.RES_LO
        mod.INST
    )
    ; source columns (in STP)
    (
        (* stp.ARG_1_HI   stp.MOD_FLAG)
        (* stp.ARG_1_LO   stp.MOD_FLAG)
        stp.ZERO
        (* stp.ARG_2_LO   stp.MOD_FLAG)
        stp.ZERO
        (* stp.RES_LO       stp.MOD_FLAG)
        (* stp.EXO_INST     stp.MOD_FLAG)
    )
)

Question. Could there be a simpler solution say where one writes directly say 0 or even stp.0 or similar ?

[delehef]

We could do that in Corset; however, we should see with @AlexandreBelling if a constant column is required, or if we can just put a scalar constant.

[AlexandreBelling]

It could be done in the prover. This will in practice translate to an appropriate smart-vector. What is inefficient is that we need to commit to that vector in the prover while it could be manipulated by the verifier directly as a scalar.

[delehef]

Addressed with (defcolumns ... (SOME_COLUMN :comp <EXPRESSION>) ...)